--- a/QuotMain.thy	Fri Aug 21 13:56:20 2009 +0200
+++ b/QuotMain.thy	Tue Aug 25 00:30:23 2009 +0200
@@ -1,7 +1,13 @@
 theory QuotMain
-imports QuotScript QuotList
+imports QuotScript QuotList Prove
 begin
 
+(*
+prove {* @{prop "True"} *}
+apply(rule TrueI)
+done
+*)
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"