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.
corrected indentation
authoroheimb
Fri, 11 Sep 1998 12:55:40 +0200
changeset 5476 1c09934fe445
parent 5475 410172655d64
child 5477 41ab0f44dd8f
corrected indentation
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite.ML	Thu Sep 10 18:07:06 1998 +0200
+++ b/src/HOL/Finite.ML	Fri Sep 11 12:55:40 1998 +0200
@@ -325,7 +325,7 @@
 by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
-by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
+ by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
 by (fast_tac (claset() addss
 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
 qed_spec_mp "card_mono";
isabelle