--- a/Quot/Examples/AbsRepTest.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -2,6 +2,52 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
+ML_command "ProofContext.debug := false"
+ML_command "ProofContext.verbose := false"
+
+ML {*
+val ctxt0 = @{context}
+val ty = Syntax.read_typ ctxt0 "bool"  
+val ctxt1 = Variable.declare_typ ty ctxt0 
+val trm = Syntax.parse_term ctxt1 "A \<and> B"
+val trm' = Syntax.type_constraint ty trm
+val trm'' = Syntax.check_term ctxt1 trm'
+val ctxt2 = Variable.declare_term trm'' ctxt1 
+*}
+
+term "split"
+
+term "Ex1 (\<lambda>(x, y). P x y)" 
+
+lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
+apply(erule ex1E)
+apply(case_tac x)
+apply(clarify)
+apply(rule_tac a="aa" in ex1I)
+apply(rule ex1I)
+apply(assumption)
+apply(blast)
+apply(blast)
+done
+
+(*
+lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
+apply(erule ex1E)
+apply(erule ex1E)
+apply(rule_tac a="(x, y)" in ex1I)
+apply(clarify)
+apply(case_tac xa)
+apply(clarify)
+
+apply(rule ex1I)
+apply(assumption)
+apply(blast)
+apply(blast)
+done
+
+apply(metis)
+*)
+
 ML {* open Quotient_Term *}
 
 ML {*