Quot/Examples/FSet.thy
changeset 627 88f831f86b96
parent 626 28e9c770a082
child 631 e26e3dac3bf0
--- a/Quot/Examples/FSet.thy	Tue Dec 08 13:08:56 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 13:09:21 2009 +0100
@@ -446,7 +446,7 @@
 sorry
 
 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
-apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *})
+(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
 end