content: --
  -- Copyright 2016, NICTA
  --
  -- This software may be distributed and modified according to the terms of
  -- the GNU General Public License version 2. Note that NO WARRANTY is provided.
  -- See "LICENSE_GPLv2.txt" for details.
  --
  -- @TAG(NICTA_GPL)
  --
  
  {-# LANGUAGE QuasiQuotes #-}
  module Isabelle.TestTH where
  
  import Text.PrettyPrint.ANSI.Leijen
  import Isabelle.InnerAST
  import Isabelle.OuterAST
  import Isabelle.ExprTH
  
  val :: Theory Type Term
  val = let theoryName = "Test"
            defName = "deffo"
            typ = [isaType| int \<times> int \<Rightarrow> int |]
            term = [isaTerm| (\<lambda>x. x) y |]
  
          in [isaTheory|
           theory $theoryName
           imports Main
           begin
             type_synonym n = "nat"
             definition "(B \<or> C) \<and> D"
             definition "B \<or> (C \<and> D)"
             definition "(A \<equiv> B) \<longrightarrow> C"
             definition "A \<equiv> (B \<longrightarrow> C)"
             definition "\<exists> a b c. (A \<longrightarrow> C)"
             definition "(\<exists> a b c. A) \<longrightarrow> C"
             definition "True"
             definition "A x \<equiv> B x"
             definition "\<lambda>x. (x y)"
             definition "$term"
             definition "((\<lambda>x. x) y) \<equiv> (B (x y))"
  
             definition x :: "'a \<Rightarrow> 'b" where "A"
             definition $defName :: "$typ" where "A"
             definition x :: "int \<times> (int \<Rightarrow> int)" where "A"
             definition x :: "'a option \<Rightarrow> 'b" where "A"
             definition x :: "('a, ('b \<times> 'e) \<times> 'd) test \<Rightarrow> 'c" where "A"
             definition "A :: bool \<equiv> B"
  
             lemma lemma1[attribute1, attribute2 with args]: "A \<and> B"
               apply clarsimp
               done
  
             lemma "A \<longrightarrow> B"
               apply (clarsimp simp: blah foo bar dest: baz, clarsimp, (clarsimp | clarsimp))?
               sorry
  
           end
         |]
  
  main :: IO ()
  main = putDoc . pretty $ val
  