src/ZF/Finite.ML
 changeset 1461 6bcb44e4d6e5 parent 803 4c8333ab3eae child 1956 589af052bcd4
```--- a/src/ZF/Finite.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Finite.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/Finite.ML
+(*  Title:      ZF/Finite.ML
ID:         \$Id\$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Finite powerset operator; finite function space
@@ -33,7 +33,7 @@
\    |] ==> P(b)";
by (rtac (major RS Fin.induct) 1);
by (excluded_middle_tac "a:b" 2);
-by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
+by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
by (REPEAT (ares_tac prems 1));
qed "Fin_induct";

@@ -68,19 +68,19 @@
qed "Fin_subset";

val major::prems = goal Finite.thy
-    "[| c: Fin(A);  b: Fin(A);  				\
-\       P(b);       						\
+    "[| c: Fin(A);  b: Fin(A);                                  \
+\       P(b);                                                   \
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
\    |] ==> c<=b --> P(b-c)";
by (rtac (major RS Fin_induct) 1);
by (rtac (Diff_cons RS ssubst) 2);
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
-				Diff_subset RS Fin_subset]))));
+                                Diff_subset RS Fin_subset]))));
qed "Fin_0_induct_lemma";

val prems = goal Finite.thy
-    "[| b: Fin(A);  						\
-\       P(b);        						\
+    "[| b: Fin(A);                                              \
+\       P(b);                                                   \
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
\    |] ==> P(0)";
by (rtac (Diff_cancel RS subst) 1);```