Mercurial Mercurial > repos > Old_HOL / 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.
Updated simpsets and a few proofs.
authornipkow
Tue, 22 Mar 1994 08:32:22 +0100
changeset 58 1322cef1a4d8
parent 57 194d088c1511
child 59 38e2eaa2219f
Updated simpsets and a few proofs.
ex/Finite.ML file | annotate | diff | comparison | revisions
ex/finite.ML file | annotate | diff | comparison | revisions 
--- a/ex/Finite.ML	Tue Mar 22 08:31:58 1994 +0100
+++ b/ex/Finite.ML	Tue Mar 22 08:32:22 1994 +0100
@@ -86,8 +86,8 @@
 \    |] ==> c<=b --> P(b-c)";
 by (rtac (major RS Fin_induct) 1);
 by (rtac (Diff_insert RS ssubst) 2);
-by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, 
-				Diff_subset RS Fin_subset]))));
+by (ALLGOALS (asm_simp_tac
+                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
 val Fin_empty_induct_lemma = result();
 
 val prems = goal Finite.thy 
--- a/ex/finite.ML	Tue Mar 22 08:31:58 1994 +0100
+++ b/ex/finite.ML	Tue Mar 22 08:32:22 1994 +0100
@@ -86,8 +86,8 @@
 \    |] ==> c<=b --> P(b-c)";
 by (rtac (major RS Fin_induct) 1);
 by (rtac (Diff_insert RS ssubst) 2);
-by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, 
-				Diff_subset RS Fin_subset]))));
+by (ALLGOALS (asm_simp_tac
+                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
 val Fin_empty_induct_lemma = result();
 
 val prems = goal Finite.thy
Old_HOL