Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Made fset work again to test all.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 08 Dec 2009 13:09:21 +0100
changeset 627 88f831f86b96
parent 626 28e9c770a082
child 628 a11b9b757f89
child 629 df42285e7286
Made fset work again to test all.
Quot/Examples/FSet.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2