# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260290612 -3600
# Node ID 005e4edc65ef5ea5bbf56daf3cecb04d206f9487
# Parent  b98d64dc98d9ce20bd7a0119c9085506526c7fb6# Parent  5cb44fe9ae8e4c2dbcf91d680c36c7365130cabe
merged

diff -r 5cb44fe9ae8e -r 005e4edc65ef Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 17:39:34 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:43:32 2009 +0100
@@ -307,10 +307,7 @@
 by (tactic {* lift_tac @{context} @{thm m2} 1 *})
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (tactic {* procedure_tac @{context} @{thm list_eq.intros(4)} 1 *})
-apply (regularize)
-apply (injection)
-apply (cleaning)
+apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *})
 done
 
 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
@@ -432,14 +429,12 @@
 sorry
 
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
-apply(lifting_setup ttt2)
+apply(lifting ttt2)
 apply(regularize)
 apply(rule impI)
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(injection)
-apply(tactic {* clean_tac @{context} 1 *}) (* This is an example that needs lambda_prs twice *)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
diff -r 5cb44fe9ae8e -r 005e4edc65ef Quot/QuotMain.thy