--- a/src/ZF/ex/Brouwer.ML Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Brouwer.ML Mon May 21 14:36:24 2001 +0200
@@ -20,10 +20,10 @@
(*A nicer induction rule than the standard one*)
val major::prems = goal Brouwer.thy
- "[| b: brouwer; \
+ "[| b \\<in> brouwer; \
\ P(Zero); \
-\ !!b. [| b: brouwer; P(b) |] ==> P(Suc(b)); \
-\ !!h. [| h: nat -> brouwer; ALL i:nat. P(h`i) \
+\ !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b)); \
+\ !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i) \
\ |] ==> P(Lim(h)) \
\ |] ==> P(b)";
by (rtac (major RS brouwer.induct) 1);
@@ -35,7 +35,7 @@
(** The Martin-Löf wellordering type **)
-Goal "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
+Goal "Well(A,B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A,B))";
let open Well; val rew = rewrite_rule con_defs in
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
end;
@@ -43,8 +43,8 @@
(*A nicer induction rule than the standard one*)
val major::prems = goal Brouwer.thy
- "[| w: Well(A,B); \
-\ !!a f. [| a: A; f: B(a) -> Well(A,B); ALL y: B(a). P(f`y) \
+ "[| w \\<in> Well(A,B); \
+\ !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y) \
\ |] ==> P(Sup(a,f)) \
\ |] ==> P(w)";
by (rtac (major RS Well.induct) 1);