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.
added indentation
authoroheimb
Mon, 21 Sep 1998 15:58:27 +0200
changeset 5516 d80e9aeb4a2b
parent 5515 903c956beac3
child 5517 863f56450888
added indentation
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite.ML	Mon Sep 21 12:01:14 1998 +0200
+++ b/src/HOL/Finite.ML	Mon Sep 21 15:58:27 1998 +0200
@@ -187,8 +187,8 @@
  by (etac finite_imageI 1);
 by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
 by Auto_tac;
- by (rtac bexI 1);
- by (assume_tac 2);
+by (rtac bexI 1);
+by  (assume_tac 2);
 by (Simp_tac 1);
 qed "finite_converse";
 AddIffs [finite_converse];
isabelle