# HG changeset patch
# User paulson
# Date 990449190 -7200
# Node ID 6536fb8c9fc6d6abcfa5e7fdd6500900d3c559b7
# Parent  7f9e4c3893181a89213d73d2ff73369c27344322
X-symbols for ZF

diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/BCR.thy	Mon May 21 14:46:30 2001 +0200
@@ -21,7 +21,7 @@
 defs
   isofenv_def "isofenv(ve,te) ==                
    ve_dom(ve) = te_dom(te) &            
-   ( ALL x:ve_dom(ve).                          
-     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+   ( \\<forall>x \\<in> ve_dom(ve).                          
+     \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   
 end
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Dynamic.thy	Mon May 21 14:46:30 2001 +0200
@@ -12,25 +12,25 @@
   domains "EvalRel" <= "ValEnv * Exp * Val"
   intrs
     eval_constI
-      " [| ve:ValEnv; c:Const |] ==>   
+      " [| ve \\<in> ValEnv; c \\<in> Const |] ==>   
        <ve,e_const(c),v_const(c)>:EvalRel"
     eval_varI
-      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>   
        <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
     eval_fnI
-      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>   
        <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
     eval_fixI
-      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   
+      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;   
           v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
        <ve,e_fix(f,x,e),cl>:EvalRel " 
     eval_appI1
-      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   
+      " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;   
           <ve,e1,v_const(c1)>:EvalRel;   
           <ve,e2,v_const(c2)>:EvalRel |] ==>   
        <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
     eval_appI2
-      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   
+      " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;   
           <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
           <ve,e2,v2>:EvalRel;   
           <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/ECR.ML
--- a/src/ZF/Coind/ECR.ML	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/ECR.ML	Mon May 21 14:46:30 2001 +0200
@@ -6,9 +6,9 @@
 
 (* Specialised co-induction rule *)
 
-Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;  \
+Goal "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv;  \
 \        <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
-\        {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
+\        {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}: \
 \        Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]    \
 \     ==> <v_clos(x, e, ve),t>:HasTyRel";
 by (rtac (singletonI RS HasTyRel.coinduct) 1);
@@ -40,7 +40,7 @@
 	  HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
 
 Goalw [hastyenv_def]
-  "[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
+  "[| ve \\<in> ValEnv; te \\<in> TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
 \   hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
 by (asm_full_simp_tac
     (simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
@@ -48,7 +48,7 @@
 qed "hastyenv_owr";
 
 Goalw  [isofenv_def,hastyenv_def]
-  "[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
+  "[| ve \\<in> ValEnv; te \\<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
 by Safe_tac;
 by (dtac bspec 1);
 by (assume_tac 1);
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/ECR.thy	Mon May 21 14:46:30 2001 +0200
@@ -14,12 +14,12 @@
   domains "HasTyRel" <= "Val * Ty"
   intrs
     htr_constI
-      "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
+      "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
     htr_closI
-      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
+      "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; 
           <te,e_fn(x,e),t>:ElabRel;  
           ve_dom(ve) = te_dom(te);   
-          {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
+          {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)  
       |] ==>   
       <v_clos(x,e,ve),t>:HasTyRel" 
   monos  Pow_mono
@@ -33,6 +33,6 @@
   hastyenv_def 
     " hastyenv(ve,te) ==                        
      ve_dom(ve) = te_dom(te) &          
-     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+     (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
 
 end
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Language.thy	Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
   c_app :: [i,i] => i           (*Abstract constructor for fun application*)
 
 rules
-  constNEE  "c:Const ==> c ~= 0"
-  c_appI    "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+  constNEE  "c \\<in> Const ==> c \\<noteq> 0"
+  c_appI    "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
 
 
 consts
@@ -20,10 +20,10 @@
   ExVar :: i                    (* Abstract type of variables *)
 
 datatype
-  "Exp" = e_const ("c:Const")
-        | e_var ("x:ExVar")
-        | e_fn ("x:ExVar","e:Exp")
-        | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
-        | e_app ("e1:Exp","e2:Exp")
+  "Exp" = e_const ("c \\<in> Const")
+        | e_var ("x \\<in> ExVar")
+        | e_fn ("x \\<in> ExVar","e \\<in> Exp")
+        | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
+        | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
 
 end
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/MT.ML	Mon May 21 14:46:30 2001 +0200
@@ -8,23 +8,23 @@
 (* The Consistency theorem                                      *)
 (* ############################################################ *)
 
-Goal "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==>         \
-\       <v_const(c), t> : HasTyRel";
+Goal "[| c \\<in> Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==>         \
+\       <v_const(c), t> \\<in> HasTyRel";
 by (Fast_tac 1);
 qed "consistency_const";
 
 
 Goalw [hastyenv_def]
-  "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==>     \
+  "[| x \\<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==>     \
 \  <ve_app(ve,x),t>:HasTyRel";
 by (Fast_tac 1);
 qed "consistency_var";
 
 
 Goalw [hastyenv_def]
-  "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te);       \
+  "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; hastyenv(ve,te);       \
 \          <te,e_fn(x,e),t>:ElabRel  \
-\       |] ==> <v_clos(x, e, ve), t> : HasTyRel";
+\       |] ==> <v_clos(x, e, ve), t> \\<in> HasTyRel";
 by (Blast_tac 1);
 qed "consistency_fn";
 
@@ -40,7 +40,7 @@
     (ematch_tac [te_owrE] i));
 
 Goalw [hastyenv_def]
-  "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;               \
+  "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;               \
 \     v_clos(x,e,ve_owr(ve,f,cl)) = cl;                         \ 
 \     hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==>       \
 \  <cl,t>:HasTyRel";
@@ -75,12 +75,12 @@
 qed "consistency_fix";
 
 
-Goal "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
+Goal "[| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;   \
 \     <ve,e1,v_const(c1)>:EvalRel;                      \
-\     ALL t te.                                         \
+\     \\<forall>t te.                                         \
 \       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
-\     <ve, e2, v_const(c2)> : EvalRel;                  \
-\     ALL t te.                                         \
+\     <ve, e2, v_const(c2)> \\<in> EvalRel;                  \
+\     \\<forall>t te.                                         \
 \       hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
 \     hastyenv(ve, te);                                 \
 \     <te,e_app(e1,e2),t>:ElabRel |] ==>                \
@@ -89,19 +89,19 @@
 by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
 qed "consistency_app1";
 
-Goal "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
+Goal "[| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;  \
 \        <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
-\        ALL t te.                                \
+\        \\<forall>t te.                                \
 \          hastyenv(ve,te) -->                    \
 \          <te,e1,t>:ElabRel -->                  \
 \          <v_clos(xm,em,vem),t>:HasTyRel;        \
 \        <ve,e2,v2>:EvalRel;                      \
-\        ALL t te.                                \
+\        \\<forall>t te.                                \
 \          hastyenv(ve,te) -->                    \
 \          <te,e2,t>:ElabRel -->                  \
 \          <v2,t>:HasTyRel;                       \
 \        <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
-\        ALL t te.                                \
+\        \\<forall>t te.                                \
 \          hastyenv(ve_owr(vem,xm,v2),te) -->     \
 \          <te,em,t>:ElabRel -->                  \
 \          <v,t>:HasTyRel;                        \
@@ -130,14 +130,14 @@
 qed "consistency_app2";
 
 Goal "<ve,e,v>:EvalRel ==>         \
-\       (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
+\       (\\<forall>t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
 by (etac EvalRel.induct 1);
 by (blast_tac (claset() addIs [consistency_app2]) 6);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
 qed "consistency";
 
 
-Goal "[| ve:ValEnv; te:TyEnv;              \
+Goal "[| ve \\<in> ValEnv; te \\<in> TyEnv;              \
 \        isofenv(ve,te);                   \
 \        <ve,e,v_const(c)>:EvalRel;        \
 \        <te,e,t>:ElabRel                  \
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Map.ML	Mon May 21 14:46:30 2001 +0200
@@ -6,21 +6,21 @@
 
 (** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
 
-Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})";
+Goalw [TMap_def] "{0,1} \\<subseteq> {1} Un TMap(I, {0,1})";
 by (Blast_tac 1);
 result();
 
-Goalw [TMap_def] "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))";
+Goalw [TMap_def] "{0} Un TMap(I,1) \\<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))";
 by (Blast_tac 1);
 result();
 
-Goalw [TMap_def] "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))";
+Goalw [TMap_def] "{0,1} Un TMap(I,2) \\<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))";
 by (Blast_tac 1);
 result();
 
 (*
 Goalw [TMap_def]
-     "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
+     "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \\<subseteq> \
 \     {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
 by (Blast_tac 1);
 result();
@@ -31,19 +31,19 @@
 (* Lemmas                                                       *)
 (* ############################################################ *)
 
-Goal "Sigma(A,B)``{a} = (if a:A then B(a) else 0)";
+Goal "Sigma(A,B)``{a} = (if a \\<in> A then B(a) else 0)";
 by Auto_tac;
 qed "qbeta_if";
 
-Goal "a:A ==> Sigma(A,B)``{a} = B(a)";
+Goal "a \\<in> A ==> Sigma(A,B)``{a} = B(a)";
 by (Fast_tac 1);
 qed "qbeta";
 
-Goal "a~:A ==> Sigma(A,B)``{a} = 0";
+Goal "a\\<notin>A ==> Sigma(A,B)``{a} = 0";
 by (Fast_tac 1);
 qed "qbeta_emp";
 
-Goal "a ~: A ==> Sigma(A,B)``{a}=0";
+Goal "a \\<notin> A ==> Sigma(A,B)``{a}=0";
 by (Fast_tac 1);
 qed "image_Sigma1";
 
@@ -55,7 +55,7 @@
 (* Lemmas *)
 
 Goalw [quniv_def]
-    "A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
+    "A \\<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \\<subseteq> quniv(X)";
 by (rtac Pow_mono 1);
 by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
 by (etac subset_trans 1);
@@ -66,7 +66,7 @@
 (* Theorems *)
 
 val prems = goalw Map.thy [PMap_def,TMap_def]
-  "[| m:PMap(A,quniv(B)); !!x. x:A ==> x:univ(B) |] ==> m:quniv(B)";
+  "[| m \\<in> PMap(A,quniv(B)); !!x. x \\<in> A ==> x \\<in> univ(B) |] ==> m \\<in> quniv(B)";
 by (cut_facts_tac prems 1);
 by (rtac (MapQU_lemma RS subsetD) 1);
 by (rtac subsetI 1);
@@ -78,7 +78,7 @@
 (* Monotonicity                                                 *)
 (* ############################################################ *)
 
-Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
+Goalw [PMap_def,TMap_def] "B \\<subseteq> C ==> PMap(A,B)<=PMap(A,C)";
 by (Blast_tac 1);
 qed "map_mono";
 
@@ -90,7 +90,7 @@
 
 (** map_emp **)
 
-Goalw [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
+Goalw [map_emp_def,PMap_def,TMap_def] "map_emp \\<in> PMap(A,B)";
 by Auto_tac;
 qed "pmap_empI";
 
@@ -98,7 +98,7 @@
 
 
 Goalw [map_owr_def,PMap_def,TMap_def] 
-  "[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
+  "[| m \\<in> PMap(A,B); a \\<in> A; b \\<in> B |]  ==> map_owr(m,a,b):PMap(A,B)";
 by Safe_tac;
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff])));
 by (Fast_tac 1);
@@ -107,10 +107,10 @@
 (*Remaining subgoal*)
 by (rtac (excluded_middle RS disjE) 1);
 by (etac image_Sigma1 1);
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
+by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 1);
 by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1);
 by Safe_tac;
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
+by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 3);
 by (ALLGOALS Asm_full_simp_tac);
 by (Fast_tac 1);
 qed "pmap_owrI";
@@ -118,7 +118,7 @@
 (** map_app **)
 
 Goalw [TMap_def,map_app_def] 
-  "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
+  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a) \\<noteq>0";
 by (etac domainE 1);
 by (dtac imageI 1);
 by (Fast_tac 1);
@@ -126,12 +126,12 @@
 qed "tmap_app_notempty";
 
 Goalw [TMap_def,map_app_def,domain_def] 
-  "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
 by (Fast_tac 1);
 qed "tmap_appI";
 
 Goalw [PMap_def]
-  "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+  "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
 by (ftac tmap_app_notempty 1); 
 by (assume_tac 1);
 by (dtac tmap_appI 1); 
@@ -142,12 +142,12 @@
 (** domain **)
 
 Goalw [TMap_def]
-  "[| m:TMap(A,B); a:domain(m) |] ==> a:A";
+  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
 by (Fast_tac 1);
 qed "tmap_domainD";
 
 Goalw [PMap_def,TMap_def]
-  "[| m:PMap(A,B); a:domain(m) |] ==> a:A";
+  "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
 by (Fast_tac 1);
 qed "pmap_domainD";
 
@@ -159,11 +159,11 @@
 
 (* Lemmas *)
 
-Goal  "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))";
+Goal  "domain(\\<Union>x \\<in> A. B(x)) = (\\<Union>x \\<in> A. domain(B(x)))";
 by (Fast_tac 1);
 qed "domain_UN";
 
-Goal  "domain(Sigma(A,B)) = {x:A. EX y. y:B(x)}";
+Goal  "domain(Sigma(A,B)) = {x \\<in> A. \\<exists>y. y \\<in> B(x)}";
 by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1);
 by (Fast_tac 1);
 qed "domain_Sigma";
@@ -175,7 +175,7 @@
 qed "map_domain_emp";
 
 Goalw [map_owr_def] 
-  "b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
+  "b \\<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
 by (simp_tac (simpset() addsimps [domain_Sigma]) 1);
 by (rtac equalityI 1);
 by (Fast_tac 1);
@@ -201,6 +201,6 @@
 by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
 qed "map_app_owr1";
 
-Goal "c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+Goal "c \\<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
 by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
 qed "map_app_owr2";
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Map.thy	Mon May 21 14:46:30 2001 +0200
@@ -6,23 +6,21 @@
 
 Map = QUniv +
 
-consts
+constdefs
   TMap :: [i,i] => i
+   "TMap(A,B) == {m \\<in> Pow(A*Union(B)).\\<forall>a \\<in> A. m``{a} \\<in> B}"
+
   PMap :: [i,i] => i
-defs
-  TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A. m``{a}:B}"
-  PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
+   "PMap(A,B) == TMap(A,cons(0,B))"
 
-(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
+(* Note: 0 \\<in> B ==> TMap(A,B) = PMap(A,B) *)
   
-consts
   map_emp :: i
+   "map_emp == 0"
+
   map_owr :: [i,i,i]=>i
+   "map_owr(m,a,b) == \\<Sigma>x \\<in> {a} Un domain(m). if x=a then b else m``{x}"
   map_app :: [i,i]=>i
-defs
-  map_emp_def "map_emp == 0"
-  map_owr_def "map_owr(m,a,b) ==
-	         SUM x:{a} Un domain(m). if x=a then b else m``{x}"
-  map_app_def "map_app(m,a) == m``{a}"
+   "map_app(m,a) == m``{a}"
   
 end
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Static.thy	Mon May 21 14:46:30 2001 +0200
@@ -12,21 +12,21 @@
   domains "ElabRel" <= "TyEnv * Exp * Ty"
   intrs
     constI
-      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
+      " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==>   
        <te,e_const(c),t>:ElabRel "
     varI
-      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
+      " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==>   
        <te,e_var(x),te_app(te,x)>:ElabRel "
     fnI
-      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
+      " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;   
           <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
        <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
     fixI
-      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
+      " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty;   
           <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
        <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
     appI
-      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
+      " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;   
           <te,e1,t_fun(t1,t2)>:ElabRel;   
           <te,e2,t1>:ElabRel |] ==>   
        <te,e_app(e1,e2),t2>:ElabRel "
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Types.ML
--- a/src/ZF/Coind/Types.ML	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Types.ML	Mon May 21 14:46:30 2001 +0200
@@ -10,12 +10,12 @@
 by (Simp_tac 1);
 qed "te_app_owr1";
 
-Goal "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
+Goal "x \\<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
 by Auto_tac;
 qed "te_app_owr2";
 
-Goal "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
-by (res_inst_tac [("P","x:te_dom(te)")] impE 1);
+Goal "[| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> te_app(te,x):Ty";
+by (res_inst_tac [("P","x \\<in> te_dom(te)")] impE 1);
 by (assume_tac 2);
 by (assume_tac 2);
 by (etac TyEnv.induct 1);
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Types.thy	Mon May 21 14:46:30 2001 +0200
@@ -11,8 +11,8 @@
   TyConst :: i          (* Abstract type of type constants *)
 
 datatype
-  "Ty" = t_const ("tc:TyConst")
-       | t_fun ("t1:Ty","t2:Ty")
+  "Ty" = t_const ("tc \\<in> TyConst")
+       | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
   
 
 (* Definition of type environments and associated operators *)
@@ -22,7 +22,7 @@
 
 datatype
   "TyEnv" = te_emp
-          | te_owr ("te:TyEnv","x:ExVar","t:Ty") 
+          | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty") 
 
 consts
   te_dom :: i => i
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Values.ML
--- a/src/ZF/Coind/Values.ML	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Values.ML	Mon May 21 14:46:30 2001 +0200
@@ -9,7 +9,7 @@
 (* Elimination rules *)
 
 val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
-  "[| ve:ValEnv; !!m.[| ve=ve_mk(m); m:PMap(ExVar,Val) |] ==> Q |] ==> Q";
+  "[| ve \\<in> ValEnv; !!m.[| ve=ve_mk(m); m \\<in> PMap(ExVar,Val) |] ==> Q |] ==> Q";
 by (cut_facts_tac prems 1);
 by (etac CollectE 1);
 by (etac exE 1);
@@ -20,10 +20,10 @@
 qed "ValEnvE";
 
 val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
-  "[| v:Val; \
-\     !!c. [| v = v_const(c); c:Const |] ==> Q;\
+  "[| v \\<in> Val; \
+\     !!c. [| v = v_const(c); c \\<in> Const |] ==> Q;\
 \     !!e ve x. \
-\       [| v = v_clos(x,e,ve); x:ExVar; e:Exp; ve:ValEnv |] ==> Q \
+\       [| v = v_clos(x,e,ve); x \\<in> ExVar; e \\<in> Exp; ve \\<in> ValEnv |] ==> Q \
 \  |] ==> \
 \  Q";
 by (cut_facts_tac prems 1);
@@ -43,7 +43,7 @@
 (* Nonempty sets *)
 
 Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
-  "v_clos(x,e,ve) ~= 0";
+  "v_clos(x,e,ve) \\<noteq> 0";
 by (Blast_tac 1);
 qed "v_closNE";
 
@@ -51,7 +51,7 @@
 AddSEs [v_closNE RS notE];
 
 Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
-  "c:Const ==> v_const(c) ~= 0";
+  "c \\<in> Const ==> v_const(c) \\<noteq> 0";
 by (dtac constNEE 1);
 by Auto_tac;
 qed "v_constNE";
@@ -60,32 +60,32 @@
 
 (* Proving that the empty set is not a value *)
 
-Goal "v:Val ==> v ~= 0";
+Goal "v \\<in> Val ==> v \\<noteq> 0";
 by (etac ValE 1);
 by Auto_tac;
 qed "ValNEE";
 
 (* Equalities for value environments *)
 
-Goal "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
+Goal "[| ve \\<in> ValEnv; v \\<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
 by (etac ValEnvE 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [map_domain_owr]));
 qed "ve_dom_owr";
 
-Goal "ve:ValEnv \
+Goal "ve \\<in> ValEnv \
 \     ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"; 
 by (etac ValEnvE 1);
 by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
 qed "ve_app_owr";
 
-Goal "ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; 
+Goal "ve \\<in> ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; 
 by (etac ValEnvE 1);
 by (Asm_full_simp_tac 1);
 by (rtac map_app_owr1 1);
 qed "ve_app_owr1";
 
-Goal "ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+Goal "ve \\<in> ValEnv ==> x \\<noteq> y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
 by (etac ValEnvE 1);
 by (Asm_full_simp_tac 1);
 by (rtac map_app_owr2 1);
@@ -94,7 +94,7 @@
 
 (* Introduction rules for operators on value environments *)
 
-Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
+Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> ve_app(ve,x):Val";
 by (etac ValEnvE 1);
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
@@ -103,7 +103,7 @@
 by (assume_tac 1);
 qed "ve_appI";
 
-Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
+Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> x \\<in> ExVar";
 by (etac ValEnvE 1);
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
@@ -112,12 +112,12 @@
 by (assume_tac 1);
 qed "ve_domI";
 
-Goalw [ve_emp_def] "ve_emp:ValEnv";
+Goalw [ve_emp_def] "ve_emp \\<in> ValEnv";
 by (rtac Val_ValEnv.ve_mk_I 1);
 by (rtac pmap_empI 1);
 qed "ve_empI";
 
-Goal "[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
+Goal "[|ve \\<in> ValEnv; x \\<in> ExVar; v \\<in> Val |] ==> ve_owr(ve,x,v):ValEnv";
 by (etac ValEnvE 1);
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
diff -r 7f9e4c389318 -r 6536fb8c9fc6 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Mon May 21 14:45:52 2001 +0200
+++ b/src/ZF/Coind/Values.thy	Mon May 21 14:46:30 2001 +0200
@@ -12,10 +12,10 @@
   Val, ValEnv, Val_ValEnv  :: i
 
 codatatype
-    "Val" = v_const ("c:Const")
-          | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
+    "Val" = v_const ("c \\<in> Const")
+          | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
   and
-    "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
+    "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
   monos       map_mono
   type_intrs  A_into_univ, mapQU