diff -r 64d896cc16f8 -r 689a18f9484c Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Mon Feb 15 14:58:03 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Mon Feb 15 16:28:07 2010 +0100
@@ -8,49 +8,6 @@
 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 {*