# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260274161 -3600
# Node ID 88f831f86b9647bceea14fc07dfbc52b5c678a39
# Parent  28e9c770a082ec7533c161342c57d81462403828
Made fset work again to test all.

diff -r 28e9c770a082 -r 88f831f86b96 Quot/Examples/FSet.thy
--- 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