Mercurial Mercurial > repos > isabelle / 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.
*** empty log message ***
authornipkow
Fri, 20 Feb 1998 17:57:16 +0100
changeset 4642 2d3910d6ab10
parent 4641 70a50c2a920f
child 4643 1b40fcac5a09
*** empty log message ***
src/HOLCF/Tr.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Tr.ML	Fri Feb 20 17:56:51 1998 +0100
+++ b/src/HOLCF/Tr.ML	Fri Feb 20 17:57:16 1998 +0100
@@ -134,7 +134,6 @@
 
 goal thy "(Def x = FF) = (~x)";
 by (simp_tac (simpset() addsimps [FF_def]) 1);
-by (fast_tac HOL_cs 1);
 qed"Def_bool2";
 
 goal thy "(Def x = TT) = x";
@@ -187,4 +186,4 @@
 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
 qed"adm_nFF";
 
-Addsimps [adm_nTT,adm_nFF];
\ No newline at end of file
+Addsimps [adm_nTT,adm_nFF];
isabelle