# HG changeset patch
# User paulson
# Date 1044525665 -3600
# Node ID a28a8fbc76d4a5a6199589b1ff15f50a24af69d3
# Parent  fd40c9d9076bc17e05077624f2481b7b728922b8
changed ** to ## to avoid conflict with new comment syntax

diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -47,7 +47,7 @@
   shows 
       "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
        ==> sats(A, formula_rec_fm(p,x,z), env) <-> 
-           is_formula_rec(**A, MH, nth(x,env), nth(z,env))"
+           is_formula_rec(##A, MH, nth(x,env), nth(z,env))"
 by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def 
               MH_iff_sats [THEN iff_sym])
 
@@ -62,15 +62,15 @@
   shows
   "[|nth(i,env) = x; nth(k,env) = z; 
       i \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> is_formula_rec(**A, MH, x, z) <-> sats(A, formula_rec_fm(p,i,k), env)" 
+   ==> is_formula_rec(##A, MH, x, z) <-> sats(A, formula_rec_fm(p,i,k), env)" 
 by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
 
 theorem formula_rec_reflection:
   assumes MH_reflection:
     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
-                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+                     \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)), 
-               \<lambda>i x. is_formula_rec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
+               \<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
 apply (simp (no_asm_use) only: is_formula_rec_def)
 apply (intro FOL_reflections function_reflections fun_plus_reflections
              depth_reflection is_transrec_reflection MH_reflection)
@@ -90,19 +90,19 @@
 lemma sats_satisfies_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_fm(x,y,z), env) <->
-        is_satisfies(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
               sats_formula_rec_fm)
 
 lemma satisfies_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_satisfies(**A, x, y, z) <-> sats(A, satisfies_fm(i,j,k), env)"
+       ==> is_satisfies(##A, x, y, z) <-> sats(A, satisfies_fm(i,j,k), env)"
 by (simp add: sats_satisfies_fm)
 
 theorem satisfies_reflection:
      "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_satisfies_def)
 apply (intro formula_rec_reflection satisfies_MH_reflection)
 done
@@ -163,19 +163,19 @@
 lemma sats_DPow_sats_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, DPow_sats_fm(u,x,y,z), env) <->
-        is_DPow_sats(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+        is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: DPow_sats_fm_def is_DPow_sats_def)
 
 lemma DPow_sats_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
-   ==> is_DPow_sats(**A,nu,nx,ny,nz) <->
+   ==> is_DPow_sats(##A,nu,nx,ny,nz) <->
        sats(A, DPow_sats_fm(u,x,y,z), env)"
 by simp
 
 theorem DPow_sats_reflection:
      "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
-               \<lambda>i x. is_DPow_sats(**Lset(i),f(x),g(x),h(x),g'(x))]"
+               \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold is_DPow_sats_def) 
 apply (intro FOL_reflections function_reflections extra_reflections
              satisfies_reflection)
@@ -260,9 +260,9 @@
                is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
              (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
-               mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) & 
-               pair(**Lset(i),env,p,u) &
-               is_Collect (**Lset(i), A, is_DPow_sats(**Lset(i),A,env,p), x))]"
+               mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) & 
+               pair(##Lset(i),env,p,u) &
+               is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
 apply (unfold is_Collect_def) 
 apply (intro FOL_reflections function_reflections mem_formula_reflection
           mem_list_reflection DPow_sats_reflection)
@@ -326,7 +326,7 @@
   shows 
       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
        ==> sats(A, Collect_fm(x,p,y), env) <->
-           is_Collect(**A, nth(x,env), is_P, nth(y,env))"
+           is_Collect(##A, nth(x,env), is_P, nth(y,env))"
 by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
 
 lemma Collect_iff_sats:
@@ -335,7 +335,7 @@
   shows 
   "[| nth(i,env) = x; nth(j,env) = y;
       i \<in> nat; j \<in> nat; env \<in> list(A)|]
-   ==> is_Collect(**A, x, is_P, y) <-> sats(A, Collect_fm(i,p,j), env)"
+   ==> is_Collect(##A, x, is_P, y) <-> sats(A, Collect_fm(i,p,j), env)"
 by (simp add: sats_Collect_fm [OF is_P_iff_sats])
 
 
@@ -344,9 +344,9 @@
 theorem Collect_reflection:
   assumes is_P_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
-                     \<lambda>i x. is_P(**Lset(i), f(x), g(x))]"
+                     \<lambda>i x. is_P(##Lset(i), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
-               \<lambda>i x. is_Collect(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
+               \<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
 apply (simp (no_asm_use) only: is_Collect_def)
 apply (intro FOL_reflections is_P_reflection)
 done
@@ -377,7 +377,7 @@
   shows 
       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
        ==> sats(A, Replace_fm(x,p,y), env) <->
-           is_Replace(**A, nth(x,env), is_P, nth(y,env))"
+           is_Replace(##A, nth(x,env), is_P, nth(y,env))"
 by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
 
 lemma Replace_iff_sats:
@@ -387,7 +387,7 @@
   shows 
   "[| nth(i,env) = x; nth(j,env) = y;
       i \<in> nat; j \<in> nat; env \<in> list(A)|]
-   ==> is_Replace(**A, x, is_P, y) <-> sats(A, Replace_fm(i,p,j), env)"
+   ==> is_Replace(##A, x, is_P, y) <-> sats(A, Replace_fm(i,p,j), env)"
 by (simp add: sats_Replace_fm [OF is_P_iff_sats])
 
 
@@ -396,9 +396,9 @@
 theorem Replace_reflection:
   assumes is_P_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
-                     \<lambda>i x. is_P(**Lset(i), f(x), g(x), h(x))]"
+                     \<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
-               \<lambda>i x. is_Replace(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
+               \<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
 apply (simp (no_asm_use) only: is_Replace_def)
 apply (intro FOL_reflections is_P_reflection)
 done
@@ -431,18 +431,18 @@
 lemma sats_DPow'_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, DPow'_fm(x,y), env) <->
-        is_DPow'(**A, nth(x,env), nth(y,env))"
+        is_DPow'(##A, nth(x,env), nth(y,env))"
 by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
 
 lemma DPow'_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_DPow'(**A, x, y) <-> sats(A, DPow'_fm(i,j), env)"
+       ==> is_DPow'(##A, x, y) <-> sats(A, DPow'_fm(i,j), env)"
 by (simp add: sats_DPow'_fm)
 
 theorem DPow'_reflection:
      "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
-               \<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]"
 apply (simp only: is_DPow'_def)
 apply (intro FOL_reflections function_reflections mem_formula_reflection
              mem_list_reflection Collect_reflection DPow_sats_reflection)
@@ -534,7 +534,7 @@
  "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
                           v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
-            v \<in> x & fun_apply(**Lset(i),g,v,gy) & is_DPow'(**Lset(i),gy,u))]"
+            v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]"
 by (intro FOL_reflections function_reflections DPow'_reflection)
 
 lemma strong_rep:
@@ -558,14 +558,14 @@
                      \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
                       is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
     \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
-              (\<exists>y \<in> Lset(i). pair(**Lset(i),v,y,x) &
-             is_wfrec (**Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
-                is_Replace (**Lset(i), x, \<lambda>y z. 
-                     \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(**Lset(i),f,y,gy) & 
-                      is_DPow'(**Lset(i),gy,z), r) & 
-                      big_union(**Lset(i),r,u), mr, v, y))]" 
+              (\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) &
+             is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
+                is_Replace (##Lset(i), x, \<lambda>y z. 
+                     \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & 
+                      is_DPow'(##Lset(i),gy,z), r) & 
+                      big_union(##Lset(i),r,u), mr, v, y))]" 
 apply (simp only: rex_setclass_is_bex [symmetric])
-  --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[**Lset(i)]"} within the body
+  --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
        of the @{term is_wfrec} application. *}
 apply (intro FOL_reflections function_reflections 
           is_wfrec_reflection Replace_reflection DPow'_reflection) 
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/Internalize.thy
--- a/src/ZF/Constructible/Internalize.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Internalize.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -19,18 +19,18 @@
 
 lemma sats_Inl_fm [simp]:
    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
-    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(**A, nth(x,env), nth(z,env))"
+    ==> sats(A, Inl_fm(x,z), env) <-> is_Inl(##A, nth(x,env), nth(z,env))"
 by (simp add: Inl_fm_def is_Inl_def)
 
 lemma Inl_iff_sats:
       "[| nth(i,env) = x; nth(k,env) = z;
           i \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_Inl(**A, x, z) <-> sats(A, Inl_fm(i,k), env)"
+       ==> is_Inl(##A, x, z) <-> sats(A, Inl_fm(i,k), env)"
 by simp
 
 theorem Inl_reflection:
      "REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
-               \<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
+               \<lambda>i x. is_Inl(##Lset(i),f(x),h(x))]"
 apply (simp only: is_Inl_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -48,18 +48,18 @@
 
 lemma sats_Inr_fm [simp]:
    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
-    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(**A, nth(x,env), nth(z,env))"
+    ==> sats(A, Inr_fm(x,z), env) <-> is_Inr(##A, nth(x,env), nth(z,env))"
 by (simp add: Inr_fm_def is_Inr_def)
 
 lemma Inr_iff_sats:
       "[| nth(i,env) = x; nth(k,env) = z;
           i \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_Inr(**A, x, z) <-> sats(A, Inr_fm(i,k), env)"
+       ==> is_Inr(##A, x, z) <-> sats(A, Inr_fm(i,k), env)"
 by simp
 
 theorem Inr_reflection:
      "REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
-               \<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
+               \<lambda>i x. is_Inr(##Lset(i),f(x),h(x))]"
 apply (simp only: is_Inr_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -77,17 +77,17 @@
 
 lemma sats_Nil_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, Nil_fm(x), env) <-> is_Nil(**A, nth(x,env))"
+    ==> sats(A, Nil_fm(x), env) <-> is_Nil(##A, nth(x,env))"
 by (simp add: Nil_fm_def is_Nil_def)
 
 lemma Nil_iff_sats:
       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
-       ==> is_Nil(**A, x) <-> sats(A, Nil_fm(i), env)"
+       ==> is_Nil(##A, x) <-> sats(A, Nil_fm(i), env)"
 by simp
 
 theorem Nil_reflection:
      "REFLECTS[\<lambda>x. is_Nil(L,f(x)),
-               \<lambda>i x. is_Nil(**Lset(i),f(x))]"
+               \<lambda>i x. is_Nil(##Lset(i),f(x))]"
 apply (simp only: is_Nil_def)
 apply (intro FOL_reflections function_reflections Inl_reflection)
 done
@@ -108,18 +108,18 @@
 lemma sats_Cons_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, Cons_fm(x,y,z), env) <->
-       is_Cons(**A, nth(x,env), nth(y,env), nth(z,env))"
+       is_Cons(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: Cons_fm_def is_Cons_def)
 
 lemma Cons_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==>is_Cons(**A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
+       ==>is_Cons(##A, x, y, z) <-> sats(A, Cons_fm(i,j,k), env)"
 by simp
 
 theorem Cons_reflection:
      "REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_Cons(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Cons_def)
 apply (intro FOL_reflections pair_reflection Inr_reflection)
 done
@@ -137,17 +137,17 @@
 
 lemma sats_quasilist_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(**A, nth(x,env))"
+    ==> sats(A, quasilist_fm(x), env) <-> is_quasilist(##A, nth(x,env))"
 by (simp add: quasilist_fm_def is_quasilist_def)
 
 lemma quasilist_iff_sats:
       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
-       ==> is_quasilist(**A, x) <-> sats(A, quasilist_fm(i), env)"
+       ==> is_quasilist(##A, x) <-> sats(A, quasilist_fm(i), env)"
 by simp
 
 theorem quasilist_reflection:
      "REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
-               \<lambda>i x. is_quasilist(**Lset(i),f(x))]"
+               \<lambda>i x. is_quasilist(##Lset(i),f(x))]"
 apply (simp only: is_quasilist_def)
 apply (intro FOL_reflections Nil_reflection Cons_reflection)
 done
@@ -174,18 +174,18 @@
 
 lemma sats_hd_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, hd_fm(x,y), env) <-> is_hd(##A, nth(x,env), nth(y,env))"
 by (simp add: hd_fm_def is_hd_def)
 
 lemma hd_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)"
+       ==> is_hd(##A, x, y) <-> sats(A, hd_fm(i,j), env)"
 by simp
 
 theorem hd_reflection:
      "REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)), 
-               \<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_hd(##Lset(i),f(x),g(x))]"
 apply (simp only: is_hd_def)
 apply (intro FOL_reflections Nil_reflection Cons_reflection
              quasilist_reflection empty_reflection)  
@@ -210,18 +210,18 @@
 
 lemma sats_tl_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, tl_fm(x,y), env) <-> is_tl(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, tl_fm(x,y), env) <-> is_tl(##A, nth(x,env), nth(y,env))"
 by (simp add: tl_fm_def is_tl_def)
 
 lemma tl_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_tl(**A, x, y) <-> sats(A, tl_fm(i,j), env)"
+       ==> is_tl(##A, x, y) <-> sats(A, tl_fm(i,j), env)"
 by simp
 
 theorem tl_reflection:
      "REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
-               \<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_tl(##Lset(i),f(x),g(x))]"
 apply (simp only: is_tl_def)
 apply (intro FOL_reflections Nil_reflection Cons_reflection
              quasilist_reflection empty_reflection)
@@ -248,18 +248,18 @@
   shows 
       "[|z \<in> nat; env \<in> list(A)|]
        ==> sats(A, bool_of_o_fm(p,z), env) <->
-           is_bool_of_o(**A, P, nth(z,env))"
+           is_bool_of_o(##A, P, nth(z,env))"
 by (simp add: bool_of_o_fm_def is_bool_of_o_def p_iff_sats [THEN iff_sym])
 
 lemma is_bool_of_o_iff_sats:
   "[| P <-> sats(A, p, env); nth(k,env) = z; k \<in> nat; env \<in> list(A)|]
-   ==> is_bool_of_o(**A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
+   ==> is_bool_of_o(##A, P, z) <-> sats(A, bool_of_o_fm(p,k), env)"
 by (simp add: sats_bool_of_o_fm)
 
 theorem bool_of_o_reflection:
-     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
+     "REFLECTS [P(L), \<lambda>i. P(##Lset(i))] ==>
       REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
-               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
+               \<lambda>i x. is_bool_of_o(##Lset(i), P(##Lset(i),x), f(x))]"
 apply (simp (no_asm) only: is_bool_of_o_def)
 apply (intro FOL_reflections function_reflections, assumption+)
 done
@@ -298,15 +298,15 @@
   shows 
       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
        ==> sats(A, lambda_fm(p,x,y), env) <-> 
-           is_lambda(**A, nth(x,env), is_b, nth(y,env))"
+           is_lambda(##A, nth(x,env), is_b, nth(y,env))"
 by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym]) 
 
 theorem is_lambda_reflection:
   assumes is_b_reflection:
     "!!f g h. REFLECTS[\<lambda>x. is_b(L, f(x), g(x), h(x)), 
-                     \<lambda>i x. is_b(**Lset(i), f(x), g(x), h(x))]"
+                     \<lambda>i x. is_b(##Lset(i), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)), 
-               \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
+               \<lambda>i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i),x), f(x))]"
 apply (simp (no_asm_use) only: is_lambda_def)
 apply (intro FOL_reflections is_b_reflection pair_reflection)
 done
@@ -327,18 +327,18 @@
 lemma sats_Member_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, Member_fm(x,y,z), env) <->
-        is_Member(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_Member(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: Member_fm_def is_Member_def)
 
 lemma Member_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_Member(**A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
+       ==> is_Member(##A, x, y, z) <-> sats(A, Member_fm(i,j,k), env)"
 by (simp add: sats_Member_fm)
 
 theorem Member_reflection:
      "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_Member(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Member_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection)
 done
@@ -359,18 +359,18 @@
 lemma sats_Equal_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, Equal_fm(x,y,z), env) <->
-        is_Equal(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_Equal(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: Equal_fm_def is_Equal_def)
 
 lemma Equal_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_Equal(**A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
+       ==> is_Equal(##A, x, y, z) <-> sats(A, Equal_fm(i,j,k), env)"
 by (simp add: sats_Equal_fm)
 
 theorem Equal_reflection:
      "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_Equal(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Equal_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
 done
@@ -391,18 +391,18 @@
 lemma sats_Nand_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, Nand_fm(x,y,z), env) <->
-        is_Nand(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_Nand(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: Nand_fm_def is_Nand_def)
 
 lemma Nand_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_Nand(**A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
+       ==> is_Nand(##A, x, y, z) <-> sats(A, Nand_fm(i,j,k), env)"
 by (simp add: sats_Nand_fm)
 
 theorem Nand_reflection:
      "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_Nand(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_Nand_def)
 apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
 done
@@ -421,18 +421,18 @@
 lemma sats_Forall_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, Forall_fm(x,y), env) <->
-        is_Forall(**A, nth(x,env), nth(y,env))"
+        is_Forall(##A, nth(x,env), nth(y,env))"
 by (simp add: Forall_fm_def is_Forall_def)
 
 lemma Forall_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_Forall(**A, x, y) <-> sats(A, Forall_fm(i,j), env)"
+       ==> is_Forall(##A, x, y) <-> sats(A, Forall_fm(i,j), env)"
 by (simp add: sats_Forall_fm)
 
 theorem Forall_reflection:
      "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
-               \<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_Forall(##Lset(i),f(x),g(x))]"
 apply (simp only: is_Forall_def)
 apply (intro FOL_reflections pair_reflection Inr_reflection)
 done
@@ -454,18 +454,18 @@
 lemma sats_and_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, and_fm(x,y,z), env) <->
-        is_and(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_and(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: and_fm_def is_and_def)
 
 lemma is_and_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_and(**A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
+       ==> is_and(##A, x, y, z) <-> sats(A, and_fm(i,j,k), env)"
 by simp
 
 theorem is_and_reflection:
      "REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_and(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_and_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -488,18 +488,18 @@
 lemma sats_or_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, or_fm(x,y,z), env) <->
-        is_or(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_or(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: or_fm_def is_or_def)
 
 lemma is_or_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_or(**A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
+       ==> is_or(##A, x, y, z) <-> sats(A, or_fm(i,j,k), env)"
 by simp
 
 theorem is_or_reflection:
      "REFLECTS[\<lambda>x. is_or(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_or(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_or(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_or_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -521,18 +521,18 @@
 
 lemma sats_is_not_fm [simp]:
    "[| x \<in> nat; z \<in> nat; env \<in> list(A)|]
-    ==> sats(A, not_fm(x,z), env) <-> is_not(**A, nth(x,env), nth(z,env))"
+    ==> sats(A, not_fm(x,z), env) <-> is_not(##A, nth(x,env), nth(z,env))"
 by (simp add: not_fm_def is_not_def)
 
 lemma is_not_iff_sats:
       "[| nth(i,env) = x; nth(k,env) = z;
           i \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_not(**A, x, z) <-> sats(A, not_fm(i,k), env)"
+       ==> is_not(##A, x, z) <-> sats(A, not_fm(i,k), env)"
 by simp
 
 theorem is_not_reflection:
      "REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
-               \<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_not(##Lset(i),f(x),g(x))]"
 apply (simp only: is_not_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -602,7 +602,7 @@
   shows 
       "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
        ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
-           M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
+           M_is_recfun(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
 
 lemma is_recfun_iff_sats:
@@ -613,7 +613,7 @@
   shows
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
+   ==> M_is_recfun(##A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
 by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) 
 
 text{*The additional variable in the premise, namely @{term f'}, is essential.
@@ -622,9 +622,9 @@
 theorem is_recfun_reflection:
   assumes MH_reflection:
     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
-                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+                     \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), 
-             \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
+             \<lambda>i x. M_is_recfun(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: M_is_recfun_def)
 apply (intro FOL_reflections function_reflections
              restriction_reflection MH_reflection)
@@ -663,7 +663,7 @@
   shows 
       "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
        ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> 
-           is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
+           is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=z in lt_length_in_nat, assumption)  
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) 
@@ -678,15 +678,15 @@
   shows
   "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
       i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
-   ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" 
+   ==> is_wfrec(##A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" 
 by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
 
 theorem is_wfrec_reflection:
   assumes MH_reflection:
     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
-                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+                     \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), 
-               \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
+               \<lambda>i x. is_wfrec(##Lset(i), MH(##Lset(i),x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_wfrec_def)
 apply (intro FOL_reflections MH_reflection is_recfun_reflection)
 done
@@ -712,18 +712,18 @@
 lemma sats_cartprod_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, cartprod_fm(x,y,z), env) <->
-        cartprod(**A, nth(x,env), nth(y,env), nth(z,env))"
+        cartprod(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: cartprod_fm_def cartprod_def)
 
 lemma cartprod_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
+       ==> cartprod(##A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)"
 by (simp add: sats_cartprod_fm)
 
 theorem cartprod_reflection:
      "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
-               \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. cartprod(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: cartprod_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -751,18 +751,18 @@
 lemma sats_sum_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, sum_fm(x,y,z), env) <->
-        is_sum(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_sum(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: sum_fm_def is_sum_def)
 
 lemma sum_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
+       ==> is_sum(##A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
 by simp
 
 theorem sum_reflection:
      "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_sum(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_sum_def)
 apply (intro FOL_reflections function_reflections cartprod_reflection)
 done
@@ -780,18 +780,18 @@
 
 lemma sats_quasinat_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
+    ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(##A, nth(x,env))"
 by (simp add: quasinat_fm_def is_quasinat_def)
 
 lemma quasinat_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
+       ==> is_quasinat(##A, x) <-> sats(A, quasinat_fm(i), env)"
 by simp
 
 theorem quasinat_reflection:
      "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
-               \<lambda>i x. is_quasinat(**Lset(i),f(x))]"
+               \<lambda>i x. is_quasinat(##Lset(i),f(x))]"
 apply (simp only: is_quasinat_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -828,7 +828,7 @@
   shows 
       "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
        ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
-           is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
+           is_nat_case(##A, nth(x,env), is_b, nth(y,env), nth(z,env))"
 apply (frule lt_length_in_nat, assumption)
 apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym])
 done
@@ -838,7 +838,7 @@
                       sats(A, p, Cons(z, Cons(a,env))));
       nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
       i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
-   ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
+   ==> is_nat_case(##A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
 by (simp add: sats_is_nat_case_fm [of A is_b])
 
 
@@ -848,9 +848,9 @@
 theorem is_nat_case_reflection:
   assumes is_b_reflection:
     "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)),
-                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
+                     \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
-               \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
+               \<lambda>i x. is_nat_case(##Lset(i), f(x), is_b(##Lset(i), x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_nat_case_def)
 apply (intro FOL_reflections function_reflections
              restriction_reflection is_b_reflection quasinat_reflection)
@@ -884,7 +884,7 @@
   shows 
       "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
        ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
-           iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
+           iterates_MH(##A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
               is_F_iff_sats [symmetric])
@@ -900,7 +900,7 @@
   shows 
   "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
       i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
-   ==> iterates_MH(**A, is_F, v, x, y, z) <->
+   ==> iterates_MH(##A, is_F, v, x, y, z) <->
        sats(A, iterates_MH_fm(p,i',i,j,k), env)"
 by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) 
 
@@ -910,9 +910,9 @@
 theorem iterates_MH_reflection:
   assumes p_reflection:
     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
-                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+                     \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
  shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
-               \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
+               \<lambda>i x. iterates_MH(##Lset(i), p(##Lset(i),x), e(x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: iterates_MH_def)
 apply (intro FOL_reflections function_reflections is_nat_case_reflection
              restriction_reflection p_reflection)
@@ -956,7 +956,7 @@
   shows 
       "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
        ==> sats(A, is_iterates_fm(p,x,y,z), env) <->
-           is_iterates(**A, is_F, nth(x,env), nth(y,env), nth(z,env))"
+           is_iterates(##A, is_F, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=z in lt_length_in_nat, assumption)  
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: is_iterates_fm_def is_iterates_def sats_is_nat_case_fm 
@@ -975,7 +975,7 @@
   shows 
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
       i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
-   ==> is_iterates(**A, is_F, x, y, z) <->
+   ==> is_iterates(##A, is_F, x, y, z) <->
        sats(A, is_iterates_fm(p,i,j,k), env)"
 by (simp add: sats_is_iterates_fm [OF is_F_iff_sats]) 
 
@@ -985,9 +985,9 @@
 theorem is_iterates_reflection:
   assumes p_reflection:
     "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
-                     \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+                     \<lambda>i x. p(##Lset(i), h(x), f(x), g(x))]"
  shows "REFLECTS[\<lambda>x. is_iterates(L, p(L,x), f(x), g(x), h(x)),
-               \<lambda>i x. is_iterates(**Lset(i), p(**Lset(i),x), f(x), g(x), h(x))]"
+               \<lambda>i x. is_iterates(##Lset(i), p(##Lset(i),x), f(x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_iterates_def)
 apply (intro FOL_reflections function_reflections p_reflection
              is_wfrec_reflection iterates_MH_reflection)
@@ -1008,7 +1008,7 @@
 lemma sats_eclose_n_fm [simp]:
    "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
     ==> sats(A, eclose_n_fm(x,y,z), env) <->
-        is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_eclose_n(##A, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=z in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: eclose_n_fm_def is_eclose_n_def 
@@ -1018,12 +1018,12 @@
 lemma eclose_n_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
-       ==> is_eclose_n(**A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
+       ==> is_eclose_n(##A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)"
 by (simp add: sats_eclose_n_fm)
 
 theorem eclose_n_reflection:
      "REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),  
-               \<lambda>i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]"
+               \<lambda>i x. is_eclose_n(##Lset(i), f(x), g(x), h(x))]"
 apply (simp only: is_eclose_n_def)
 apply (intro FOL_reflections function_reflections is_iterates_reflection) 
 done
@@ -1046,18 +1046,18 @@
 
 lemma sats_mem_eclose_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(##A, nth(x,env), nth(y,env))"
 by (simp add: mem_eclose_fm_def mem_eclose_def)
 
 lemma mem_eclose_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> mem_eclose(**A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
+       ==> mem_eclose(##A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
 by simp
 
 theorem mem_eclose_reflection:
      "REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
-               \<lambda>i x. mem_eclose(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. mem_eclose(##Lset(i),f(x),g(x))]"
 apply (simp only: mem_eclose_def)
 apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
 done
@@ -1076,18 +1076,18 @@
 
 lemma sats_is_eclose_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(##A, nth(x,env), nth(y,env))"
 by (simp add: is_eclose_fm_def is_eclose_def)
 
 lemma is_eclose_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_eclose(**A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
+       ==> is_eclose(##A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
 by simp
 
 theorem is_eclose_reflection:
      "REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
-               \<lambda>i x. is_eclose(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_eclose(##Lset(i),f(x),g(x))]"
 apply (simp only: is_eclose_def)
 apply (intro FOL_reflections mem_eclose_reflection)
 done
@@ -1111,18 +1111,18 @@
 lemma sats_list_functor_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, list_functor_fm(x,y,z), env) <->
-        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_list_functor(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: list_functor_fm_def is_list_functor_def)
 
 lemma list_functor_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
+   ==> is_list_functor(##A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
 by simp
 
 theorem list_functor_reflection:
      "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_list_functor(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_list_functor_def)
 apply (intro FOL_reflections number1_reflection
              cartprod_reflection sum_reflection)
@@ -1148,7 +1148,7 @@
 lemma sats_list_N_fm [simp]:
    "[| x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
     ==> sats(A, list_N_fm(x,y,z), env) <->
-        is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_list_N(##A, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=z in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: list_N_fm_def is_list_N_def sats_is_iterates_fm) 
@@ -1157,12 +1157,12 @@
 lemma list_N_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
-       ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
+       ==> is_list_N(##A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)"
 by (simp add: sats_list_N_fm)
 
 theorem list_N_reflection:
      "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),  
-               \<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
+               \<lambda>i x. is_list_N(##Lset(i), f(x), g(x), h(x))]"
 apply (simp only: is_list_N_def)
 apply (intro FOL_reflections function_reflections 
              is_iterates_reflection list_functor_reflection) 
@@ -1187,18 +1187,18 @@
 
 lemma sats_mem_list_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(##A, nth(x,env), nth(y,env))"
 by (simp add: mem_list_fm_def mem_list_def)
 
 lemma mem_list_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
+       ==> mem_list(##A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
 by simp
 
 theorem mem_list_reflection:
      "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
-               \<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. mem_list(##Lset(i),f(x),g(x))]"
 apply (simp only: mem_list_def)
 apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
 done
@@ -1217,18 +1217,18 @@
 
 lemma sats_is_list_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, is_list_fm(x,y), env) <-> is_list(##A, nth(x,env), nth(y,env))"
 by (simp add: is_list_fm_def is_list_def)
 
 lemma is_list_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
+       ==> is_list(##A, x, y) <-> sats(A, is_list_fm(i,j), env)"
 by simp
 
 theorem is_list_reflection:
      "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
-               \<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_list(##Lset(i),f(x),g(x))]"
 apply (simp only: is_list_def)
 apply (intro FOL_reflections mem_list_reflection)
 done
@@ -1259,18 +1259,18 @@
 lemma sats_formula_functor_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, formula_functor_fm(x,y), env) <->
-        is_formula_functor(**A, nth(x,env), nth(y,env))"
+        is_formula_functor(##A, nth(x,env), nth(y,env))"
 by (simp add: formula_functor_fm_def is_formula_functor_def)
 
 lemma formula_functor_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y;
       i \<in> nat; j \<in> nat; env \<in> list(A)|]
-   ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
+   ==> is_formula_functor(##A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
 by simp
 
 theorem formula_functor_reflection:
      "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
-               \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_formula_functor(##Lset(i),f(x),g(x))]"
 apply (simp only: is_formula_functor_def)
 apply (intro FOL_reflections omega_reflection
              cartprod_reflection sum_reflection)
@@ -1295,7 +1295,7 @@
 lemma sats_formula_N_fm [simp]:
    "[| x < length(env); y < length(env); env \<in> list(A)|]
     ==> sats(A, formula_N_fm(x,y), env) <->
-        is_formula_N(**A, nth(x,env), nth(y,env))"
+        is_formula_N(##A, nth(x,env), nth(y,env))"
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: formula_N_fm_def is_formula_N_def sats_is_iterates_fm) 
@@ -1304,12 +1304,12 @@
 lemma formula_N_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i < length(env); j < length(env); env \<in> list(A)|]
-       ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
+       ==> is_formula_N(##A, x, y) <-> sats(A, formula_N_fm(i,j), env)"
 by (simp add: sats_formula_N_fm)
 
 theorem formula_N_reflection:
      "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),  
-               \<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
+               \<lambda>i x. is_formula_N(##Lset(i), f(x), g(x))]"
 apply (simp only: is_formula_N_def)
 apply (intro FOL_reflections function_reflections 
              is_iterates_reflection formula_functor_reflection) 
@@ -1334,17 +1334,17 @@
 
 lemma sats_mem_formula_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))"
+    ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(##A, nth(x,env))"
 by (simp add: mem_formula_fm_def mem_formula_def)
 
 lemma mem_formula_iff_sats:
       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
-       ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
+       ==> mem_formula(##A, x) <-> sats(A, mem_formula_fm(i), env)"
 by simp
 
 theorem mem_formula_reflection:
      "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
-               \<lambda>i x. mem_formula(**Lset(i),f(x))]"
+               \<lambda>i x. mem_formula(##Lset(i),f(x))]"
 apply (simp only: mem_formula_def)
 apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
 done
@@ -1363,17 +1363,17 @@
 
 lemma sats_is_formula_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))"
+    ==> sats(A, is_formula_fm(x), env) <-> is_formula(##A, nth(x,env))"
 by (simp add: is_formula_fm_def is_formula_def)
 
 lemma is_formula_iff_sats:
       "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|]
-       ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
+       ==> is_formula(##A, x) <-> sats(A, is_formula_fm(i), env)"
 by simp
 
 theorem is_formula_reflection:
      "REFLECTS[\<lambda>x. is_formula(L,f(x)),
-               \<lambda>i x. is_formula(**Lset(i),f(x))]"
+               \<lambda>i x. is_formula(##Lset(i),f(x))]"
 apply (simp only: is_formula_def)
 apply (intro FOL_reflections mem_formula_reflection)
 done
@@ -1415,7 +1415,7 @@
   shows 
       "[|x < length(env); z < length(env); env \<in> list(A)|]
        ==> sats(A, is_transrec_fm(p,x,z), env) <-> 
-           is_transrec(**A, MH, nth(x,env), nth(z,env))"
+           is_transrec(##A, MH, nth(x,env), nth(z,env))"
 apply (frule_tac x=z in lt_length_in_nat, assumption)  
 apply (frule_tac x=x in lt_length_in_nat, assumption)  
 apply (simp add: is_transrec_fm_def sats_is_wfrec_fm is_transrec_def MH_iff_sats [THEN iff_sym]) 
@@ -1432,15 +1432,15 @@
   shows
   "[|nth(i,env) = x; nth(k,env) = z; 
       i < length(env); k < length(env); env \<in> list(A)|]
-   ==> is_transrec(**A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)" 
+   ==> is_transrec(##A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)" 
 by (simp add: sats_is_transrec_fm [OF MH_iff_sats])
 
 theorem is_transrec_reflection:
   assumes MH_reflection:
     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
-                     \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+                     \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
   shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)), 
-               \<lambda>i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
+               \<lambda>i x. is_transrec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
 apply (simp (no_asm_use) only: is_transrec_def)
 apply (intro FOL_reflections function_reflections MH_reflection 
              is_wfrec_reflection is_eclose_reflection)
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -297,8 +297,8 @@
 text{*This version handles an alternative form of the bounded quantifier
       in the second argument of @{text REFLECTS}.*}
 theorem Rex_reflection':
-     "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
-      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
+     "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
+      ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
 apply (unfold setclass_def rex_def)
 apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
 done
@@ -306,7 +306,7 @@
 text{*As above.*}
 theorem Rall_reflection':
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
-      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
+      ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[##Lset(a)]. Q(a,x,z)]"
 apply (unfold setclass_def rall_def)
 apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
 done
@@ -369,18 +369,18 @@
 
 lemma sats_empty_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
+    ==> sats(A, empty_fm(x), env) <-> empty(##A, nth(x,env))"
 by (simp add: empty_fm_def empty_def)
 
 lemma empty_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
+       ==> empty(##A, x) <-> sats(A, empty_fm(i), env)"
 by simp
 
 theorem empty_reflection:
      "REFLECTS[\<lambda>x. empty(L,f(x)),
-               \<lambda>i x. empty(**Lset(i),f(x))]"
+               \<lambda>i x. empty(##Lset(i),f(x))]"
 apply (simp only: empty_def)
 apply (intro FOL_reflections)
 done
@@ -412,13 +412,13 @@
 lemma sats_upair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, upair_fm(x,y,z), env) <->
-            upair(**A, nth(x,env), nth(y,env), nth(z,env))"
+            upair(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: upair_fm_def upair_def)
 
 lemma upair_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
+       ==> upair(##A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
 by (simp add: sats_upair_fm)
 
 text{*Useful? At least it refers to "real" unordered pairs*}
@@ -433,7 +433,7 @@
 
 theorem upair_reflection:
      "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
-               \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]"
 apply (simp add: upair_def)
 apply (intro FOL_reflections)
 done
@@ -453,18 +453,18 @@
 lemma sats_pair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pair_fm(x,y,z), env) <->
-        pair(**A, nth(x,env), nth(y,env), nth(z,env))"
+        pair(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: pair_fm_def pair_def)
 
 lemma pair_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
+       ==> pair(##A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
 by (simp add: sats_pair_fm)
 
 theorem pair_reflection:
      "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
-               \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. pair(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: pair_def)
 apply (intro FOL_reflections upair_reflection)
 done
@@ -484,18 +484,18 @@
 lemma sats_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, union_fm(x,y,z), env) <->
-        union(**A, nth(x,env), nth(y,env), nth(z,env))"
+        union(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: union_fm_def union_def)
 
 lemma union_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
+       ==> union(##A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
 by (simp add: sats_union_fm)
 
 theorem union_reflection:
      "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
-               \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. union(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: union_def)
 apply (intro FOL_reflections)
 done
@@ -516,18 +516,18 @@
 lemma sats_cons_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, cons_fm(x,y,z), env) <->
-        is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_cons(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: cons_fm_def is_cons_def)
 
 lemma cons_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
+       ==> is_cons(##A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
 by simp
 
 theorem cons_reflection:
      "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_cons(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_cons_def)
 apply (intro FOL_reflections upair_reflection union_reflection)
 done
@@ -545,18 +545,18 @@
 lemma sats_succ_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, succ_fm(x,y), env) <->
-        successor(**A, nth(x,env), nth(y,env))"
+        successor(##A, nth(x,env), nth(y,env))"
 by (simp add: succ_fm_def successor_def)
 
 lemma successor_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
+       ==> successor(##A, x, y) <-> sats(A, succ_fm(i,j), env)"
 by simp
 
 theorem successor_reflection:
      "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
-               \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. successor(##Lset(i),f(x),g(x))]"
 apply (simp only: successor_def)
 apply (intro cons_reflection)
 done
@@ -574,18 +574,18 @@
 
 lemma sats_number1_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
+    ==> sats(A, number1_fm(x), env) <-> number1(##A, nth(x,env))"
 by (simp add: number1_fm_def number1_def)
 
 lemma number1_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
+       ==> number1(##A, x) <-> sats(A, number1_fm(i), env)"
 by simp
 
 theorem number1_reflection:
      "REFLECTS[\<lambda>x. number1(L,f(x)),
-               \<lambda>i x. number1(**Lset(i),f(x))]"
+               \<lambda>i x. number1(##Lset(i),f(x))]"
 apply (simp only: number1_def)
 apply (intro FOL_reflections empty_reflection successor_reflection)
 done
@@ -606,18 +606,18 @@
 lemma sats_big_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, big_union_fm(x,y), env) <->
-        big_union(**A, nth(x,env), nth(y,env))"
+        big_union(##A, nth(x,env), nth(y,env))"
 by (simp add: big_union_fm_def big_union_def)
 
 lemma big_union_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
+       ==> big_union(##A, x, y) <-> sats(A, big_union_fm(i,j), env)"
 by simp
 
 theorem big_union_reflection:
      "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
-               \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. big_union(##Lset(i),f(x),g(x))]"
 apply (simp only: big_union_def)
 apply (intro FOL_reflections)
 done
@@ -633,40 +633,40 @@
 
 lemma sats_subset_fm':
    "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
-    ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
+    ==> sats(A, subset_fm(x,y), env) <-> subset(##A, nth(x,env), nth(y,env))"
 by (simp add: subset_fm_def Relative.subset_def)
 
 theorem subset_reflection:
      "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
-               \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. subset(##Lset(i),f(x),g(x))]"
 apply (simp only: Relative.subset_def)
 apply (intro FOL_reflections)
 done
 
 lemma sats_transset_fm':
    "[|x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
+    ==> sats(A, transset_fm(x), env) <-> transitive_set(##A, nth(x,env))"
 by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
 
 theorem transitive_set_reflection:
      "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
-               \<lambda>i x. transitive_set(**Lset(i),f(x))]"
+               \<lambda>i x. transitive_set(##Lset(i),f(x))]"
 apply (simp only: transitive_set_def)
 apply (intro FOL_reflections subset_reflection)
 done
 
 lemma sats_ordinal_fm':
    "[|x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))"
+    ==> sats(A, ordinal_fm(x), env) <-> ordinal(##A,nth(x,env))"
 by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)
 
 lemma ordinal_iff_sats:
       "[| nth(i,env) = x;  i \<in> nat; env \<in> list(A)|]
-       ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)"
+       ==> ordinal(##A, x) <-> sats(A, ordinal_fm(i), env)"
 by (simp add: sats_ordinal_fm')
 
 theorem ordinal_reflection:
-     "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
+     "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(##Lset(i),f(x))]"
 apply (simp only: ordinal_def)
 apply (intro FOL_reflections transitive_set_reflection)
 done
@@ -689,18 +689,18 @@
 lemma sats_Memrel_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, Memrel_fm(x,y), env) <->
-        membership(**A, nth(x,env), nth(y,env))"
+        membership(##A, nth(x,env), nth(y,env))"
 by (simp add: Memrel_fm_def membership_def)
 
 lemma Memrel_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
+       ==> membership(##A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
 by simp
 
 theorem membership_reflection:
      "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
-               \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. membership(##Lset(i),f(x),g(x))]"
 apply (simp only: membership_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -723,18 +723,18 @@
 lemma sats_pred_set_fm [simp]:
    "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
     ==> sats(A, pred_set_fm(U,x,r,B), env) <->
-        pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
+        pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
 by (simp add: pred_set_fm_def pred_set_def)
 
 lemma pred_set_iff_sats:
       "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
           i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
-       ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
+       ==> pred_set(##A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
 by (simp add: sats_pred_set_fm)
 
 theorem pred_set_reflection:
      "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
-               \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
+               \<lambda>i x. pred_set(##Lset(i),f(x),g(x),h(x),b(x))]"
 apply (simp only: pred_set_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -758,18 +758,18 @@
 lemma sats_domain_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, domain_fm(x,y), env) <->
-        is_domain(**A, nth(x,env), nth(y,env))"
+        is_domain(##A, nth(x,env), nth(y,env))"
 by (simp add: domain_fm_def is_domain_def)
 
 lemma domain_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
+       ==> is_domain(##A, x, y) <-> sats(A, domain_fm(i,j), env)"
 by simp
 
 theorem domain_reflection:
      "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
-               \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_domain(##Lset(i),f(x),g(x))]"
 apply (simp only: is_domain_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -792,18 +792,18 @@
 lemma sats_range_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, range_fm(x,y), env) <->
-        is_range(**A, nth(x,env), nth(y,env))"
+        is_range(##A, nth(x,env), nth(y,env))"
 by (simp add: range_fm_def is_range_def)
 
 lemma range_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
+       ==> is_range(##A, x, y) <-> sats(A, range_fm(i,j), env)"
 by simp
 
 theorem range_reflection:
      "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
-               \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_range(##Lset(i),f(x),g(x))]"
 apply (simp only: is_range_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -827,18 +827,18 @@
 lemma sats_field_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, field_fm(x,y), env) <->
-        is_field(**A, nth(x,env), nth(y,env))"
+        is_field(##A, nth(x,env), nth(y,env))"
 by (simp add: field_fm_def is_field_def)
 
 lemma field_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
+       ==> is_field(##A, x, y) <-> sats(A, field_fm(i,j), env)"
 by simp
 
 theorem field_reflection:
      "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
-               \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. is_field(##Lset(i),f(x),g(x))]"
 apply (simp only: is_field_def)
 apply (intro FOL_reflections domain_reflection range_reflection
              union_reflection)
@@ -863,18 +863,18 @@
 lemma sats_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, image_fm(x,y,z), env) <->
-        image(**A, nth(x,env), nth(y,env), nth(z,env))"
+        image(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: image_fm_def Relative.image_def)
 
 lemma image_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
+       ==> image(##A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
 by (simp add: sats_image_fm)
 
 theorem image_reflection:
      "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
-               \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. image(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: Relative.image_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -898,18 +898,18 @@
 lemma sats_pre_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pre_image_fm(x,y,z), env) <->
-        pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
+        pre_image(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: pre_image_fm_def Relative.pre_image_def)
 
 lemma pre_image_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
+       ==> pre_image(##A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
 by (simp add: sats_pre_image_fm)
 
 theorem pre_image_reflection:
      "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
-               \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. pre_image(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: Relative.pre_image_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -933,18 +933,18 @@
 lemma sats_fun_apply_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, fun_apply_fm(x,y,z), env) <->
-        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
+        fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: fun_apply_fm_def fun_apply_def)
 
 lemma fun_apply_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
+       ==> fun_apply(##A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
 by simp
 
 theorem fun_apply_reflection:
      "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
-               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. fun_apply(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: fun_apply_def)
 apply (intro FOL_reflections upair_reflection image_reflection
              big_union_reflection)
@@ -965,18 +965,18 @@
 
 lemma sats_relation_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
+    ==> sats(A, relation_fm(x), env) <-> is_relation(##A, nth(x,env))"
 by (simp add: relation_fm_def is_relation_def)
 
 lemma relation_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
+       ==> is_relation(##A, x) <-> sats(A, relation_fm(i), env)"
 by simp
 
 theorem is_relation_reflection:
      "REFLECTS[\<lambda>x. is_relation(L,f(x)),
-               \<lambda>i x. is_relation(**Lset(i),f(x))]"
+               \<lambda>i x. is_relation(##Lset(i),f(x))]"
 apply (simp only: is_relation_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -1001,18 +1001,18 @@
 
 lemma sats_function_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
+    ==> sats(A, function_fm(x), env) <-> is_function(##A, nth(x,env))"
 by (simp add: function_fm_def is_function_def)
 
 lemma is_function_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
+       ==> is_function(##A, x) <-> sats(A, function_fm(i), env)"
 by simp
 
 theorem is_function_reflection:
      "REFLECTS[\<lambda>x. is_function(L,f(x)),
-               \<lambda>i x. is_function(**Lset(i),f(x))]"
+               \<lambda>i x. is_function(##Lset(i),f(x))]"
 apply (simp only: is_function_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -1039,13 +1039,13 @@
 lemma sats_typed_function_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, typed_function_fm(x,y,z), env) <->
-        typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"
+        typed_function(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: typed_function_fm_def typed_function_def)
 
 lemma typed_function_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
+   ==> typed_function(##A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
 by simp
 
 lemmas function_reflections =
@@ -1070,7 +1070,7 @@
 
 theorem typed_function_reflection:
      "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
-               \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. typed_function(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: typed_function_def)
 apply (intro FOL_reflections function_reflections)
 done
@@ -1099,18 +1099,18 @@
 lemma sats_composition_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, composition_fm(x,y,z), env) <->
-        composition(**A, nth(x,env), nth(y,env), nth(z,env))"
+        composition(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: composition_fm_def composition_def)
 
 lemma composition_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
+       ==> composition(##A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
 by simp
 
 theorem composition_reflection:
      "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
-               \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. composition(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: composition_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -1139,18 +1139,18 @@
 lemma sats_injection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, injection_fm(x,y,z), env) <->
-        injection(**A, nth(x,env), nth(y,env), nth(z,env))"
+        injection(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: injection_fm_def injection_def)
 
 lemma injection_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
+   ==> injection(##A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
 by simp
 
 theorem injection_reflection:
      "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
-               \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. injection(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: injection_def)
 apply (intro FOL_reflections function_reflections typed_function_reflection)
 done
@@ -1176,18 +1176,18 @@
 lemma sats_surjection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, surjection_fm(x,y,z), env) <->
-        surjection(**A, nth(x,env), nth(y,env), nth(z,env))"
+        surjection(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: surjection_fm_def surjection_def)
 
 lemma surjection_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
+   ==> surjection(##A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
 by simp
 
 theorem surjection_reflection:
      "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
-               \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. surjection(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: surjection_def)
 apply (intro FOL_reflections function_reflections typed_function_reflection)
 done
@@ -1208,18 +1208,18 @@
 lemma sats_bijection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, bijection_fm(x,y,z), env) <->
-        bijection(**A, nth(x,env), nth(y,env), nth(z,env))"
+        bijection(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: bijection_fm_def bijection_def)
 
 lemma bijection_iff_sats:
   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
+   ==> bijection(##A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
 by simp
 
 theorem bijection_reflection:
      "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
-               \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. bijection(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: bijection_def)
 apply (intro And_reflection injection_reflection surjection_reflection)
 done
@@ -1244,18 +1244,18 @@
 lemma sats_restriction_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, restriction_fm(x,y,z), env) <->
-        restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
+        restriction(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: restriction_fm_def restriction_def)
 
 lemma restriction_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
+       ==> restriction(##A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
 by simp
 
 theorem restriction_reflection:
      "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
-               \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. restriction(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: restriction_def)
 apply (intro FOL_reflections pair_reflection)
 done
@@ -1291,7 +1291,7 @@
 lemma sats_order_isomorphism_fm [simp]:
    "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
     ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
-        order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
+        order_isomorphism(##A, nth(U,env), nth(r,env), nth(B,env),
                                nth(s,env), nth(f,env))"
 by (simp add: order_isomorphism_fm_def order_isomorphism_def)
 
@@ -1299,13 +1299,13 @@
   "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
       nth(k',env) = f;
       i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
-   ==> order_isomorphism(**A,U,r,B,s,f) <->
+   ==> order_isomorphism(##A,U,r,B,s,f) <->
        sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
 by simp
 
 theorem order_isomorphism_reflection:
      "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
-               \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
+               \<lambda>i x. order_isomorphism(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
 apply (simp only: order_isomorphism_def)
 apply (intro FOL_reflections function_reflections bijection_reflection)
 done
@@ -1332,18 +1332,18 @@
 
 lemma sats_limit_ordinal_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
+    ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(##A, nth(x,env))"
 by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
 
 lemma limit_ordinal_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
+       ==> limit_ordinal(##A, x) <-> sats(A, limit_ordinal_fm(i), env)"
 by simp
 
 theorem limit_ordinal_reflection:
      "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
-               \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
+               \<lambda>i x. limit_ordinal(##Lset(i),f(x))]"
 apply (simp only: limit_ordinal_def)
 apply (intro FOL_reflections ordinal_reflection
              empty_reflection successor_reflection)
@@ -1367,18 +1367,18 @@
 
 lemma sats_finite_ordinal_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))"
+    ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(##A, nth(x,env))"
 by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)
 
 lemma finite_ordinal_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)"
+       ==> finite_ordinal(##A, x) <-> sats(A, finite_ordinal_fm(i), env)"
 by simp
 
 theorem finite_ordinal_reflection:
      "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
-               \<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
+               \<lambda>i x. finite_ordinal(##Lset(i),f(x))]"
 apply (simp only: finite_ordinal_def)
 apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
 done
@@ -1399,18 +1399,18 @@
 
 lemma sats_omega_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
-    ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
+    ==> sats(A, omega_fm(x), env) <-> omega(##A, nth(x,env))"
 by (simp add: omega_fm_def omega_def)
 
 lemma omega_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; env \<in> list(A)|]
-       ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
+       ==> omega(##A, x) <-> sats(A, omega_fm(i), env)"
 by simp
 
 theorem omega_reflection:
      "REFLECTS[\<lambda>x. omega(L,f(x)),
-               \<lambda>i x. omega(**Lset(i),f(x))]"
+               \<lambda>i x. omega(##Lset(i),f(x))]"
 apply (simp only: omega_def)
 apply (intro FOL_reflections limit_ordinal_reflection)
 done
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/Rank_Separation.thy
--- a/src/ZF/Constructible/Rank_Separation.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -21,7 +21,7 @@
   "REFLECTS[\<lambda>x. x\<in>A -->
                 (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
         \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
-                fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
+                fun_apply(##Lset(i),f,x,y) & pair(##Lset(i),y,x,p) & p \<in> r)]"
 by (intro FOL_reflections function_reflections)
 
 lemma well_ord_iso_separation:
@@ -42,8 +42,8 @@
              ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
              order_isomorphism(L,par,r,x,mx,g),
         \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
-             ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
-             order_isomorphism(**Lset(i),par,r,x,mx,g)]"
+             ordinal(##Lset(i),x) & membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+             order_isomorphism(##Lset(i),par,r,x,mx,g)]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
 lemma obase_separation:
@@ -66,9 +66,9 @@
                 membership(L,y,my) & pred_set(L,A,x,r,pxr) &
                 order_isomorphism(L,pxr,r,y,my,g))),
         \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
-                ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
-                membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
-                order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
+                ordinal(##Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
+                membership(##Lset(i),y,my) & pred_set(##Lset(i),A,x,r,pxr) &
+                order_isomorphism(##Lset(i),pxr,r,y,my,g)))]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
 lemma obase_equals_separation:
@@ -91,9 +91,9 @@
      pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
  \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
         \<exists>par \<in> Lset(i).
-         ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
-         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
-         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
+         ordinal(##Lset(i),x) & pair(##Lset(i),a,x,z) &
+         membership(##Lset(i),x,mx) & pred_set(##Lset(i),A,a,r,par) &
+         order_isomorphism(##Lset(i),par,r,x,mx,g))]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
 lemma omap_replacement:
@@ -135,9 +135,9 @@
 lemma wfrank_Reflects:
  "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
               ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
-      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
+      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
          ~ (\<exists>f \<in> Lset(i).
-            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
+            M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y),
                         rplus, x, f))]"
 by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
 
@@ -160,10 +160,10 @@
                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
                         is_range(L,f,y))),
  \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
-      (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
-       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
-         M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
-         is_range(**Lset(i),f,y)))]"
+      (\<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
+       (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(##Lset(i),x,y,z)  &
+         M_is_recfun(##Lset(i), %x f y. is_range(##Lset(i),f,y), rplus, x, f) &
+         is_range(##Lset(i),f,y)))]"
 by (intro FOL_reflections function_reflections fun_plus_reflections
              is_recfun_reflection tran_closure_reflection)
 
@@ -191,12 +191,12 @@
              is_range(L,f,rangef) -->
              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
              ordinal(L,rangef)),
-      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
+      \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(##Lset(i),r,rplus) -->
           ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
-             is_range(**Lset(i),f,rangef) -->
-             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
+             is_range(##Lset(i),f,rangef) -->
+             M_is_recfun(##Lset(i), \<lambda>x f y. is_range(##Lset(i),f,y),
                          rplus, x, f) -->
-             ordinal(**Lset(i),rangef))]"
+             ordinal(##Lset(i),rangef))]"
 by (intro FOL_reflections function_reflections is_recfun_reflection
           tran_closure_reflection ordinal_reflection)
 
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -56,18 +56,18 @@
 lemma sats_rtran_closure_mem_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
-        rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
+        rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
 
 lemma rtran_closure_mem_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
+       ==> rtran_closure_mem(##A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
 by (simp add: sats_rtran_closure_mem_fm)
 
 lemma rtran_closure_mem_reflection:
      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
-               \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: rtran_closure_mem_def)
 apply (intro FOL_reflections function_reflections fun_plus_reflections)
 done
@@ -100,18 +100,18 @@
 lemma sats_rtran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_fm(x,y), env) <->
-        rtran_closure(**A, nth(x,env), nth(y,env))"
+        rtran_closure(##A, nth(x,env), nth(y,env))"
 by (simp add: rtran_closure_fm_def rtran_closure_def)
 
 lemma rtran_closure_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
+       ==> rtran_closure(##A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
 by simp
 
 theorem rtran_closure_reflection:
      "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
-               \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]"
 apply (simp only: rtran_closure_def)
 apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
 done
@@ -132,18 +132,18 @@
 lemma sats_tran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, tran_closure_fm(x,y), env) <->
-        tran_closure(**A, nth(x,env), nth(y,env))"
+        tran_closure(##A, nth(x,env), nth(y,env))"
 by (simp add: tran_closure_fm_def tran_closure_def)
 
 lemma tran_closure_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
-       ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
+       ==> tran_closure(##A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
 by simp
 
 theorem tran_closure_reflection:
      "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
-               \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
+               \<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]"
 apply (simp only: tran_closure_def)
 apply (intro FOL_reflections function_reflections
              rtran_closure_reflection composition_reflection)
@@ -156,7 +156,7 @@
   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                  w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
-       w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
+       w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) &
        wx \<in> rp]"
 by (intro FOL_reflections function_reflections fun_plus_reflections
           tran_closure_reflection)
@@ -199,10 +199,10 @@
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
          is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
-         is_wfrec(**Lset(i),
-                  iterates_MH(**Lset(i),
-                          is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
+         is_wfrec(##Lset(i),
+                  iterates_MH(##Lset(i),
+                          is_list_functor(##Lset(i), A), 0), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection list_functor_reflection)
 
@@ -225,7 +225,7 @@
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, is_list_functor(L, A), 0, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
-               is_iterates(**Lset(i), is_list_functor(**Lset(i), A), 0, u, x)]"
+               is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]"
 by (intro FOL_reflections 
           is_iterates_reflection list_functor_reflection)
 
@@ -251,10 +251,10 @@
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
-         is_wfrec(**Lset(i),
-                  iterates_MH(**Lset(i),
-                          is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+         is_wfrec(##Lset(i),
+                  iterates_MH(##Lset(i),
+                          is_formula_functor(##Lset(i)), 0), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection formula_functor_reflection)
 
@@ -275,7 +275,7 @@
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, is_formula_functor(L), 0, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
-               is_iterates(**Lset(i), is_formula_functor(**Lset(i)), 0, u, x)]"
+               is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]"
 by (intro FOL_reflections 
           is_iterates_reflection formula_functor_reflection)
 
@@ -310,7 +310,7 @@
 lemma sats_nth_fm [simp]:
    "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, nth_fm(x,y,z), env) <->
-        is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_nth(##A, nth(x,env), nth(y,env), nth(z,env))"
 apply (frule lt_length_in_nat, assumption)  
 apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) 
 done
@@ -318,12 +318,12 @@
 lemma nth_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
-       ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
+       ==> is_nth(##A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
 by (simp add: sats_nth_fm)
 
 theorem nth_reflection:
      "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
-               \<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
+               \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]"
 apply (simp only: is_nth_def)
 apply (intro FOL_reflections is_iterates_reflection
              hd_reflection tl_reflection) 
@@ -338,10 +338,10 @@
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
-         is_wfrec(**Lset(i),
-                  iterates_MH(**Lset(i),
-                          is_tl(**Lset(i)), z), memsn, u, y))]"
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+         is_wfrec(##Lset(i),
+                  iterates_MH(##Lset(i),
+                          is_tl(##Lset(i)), z), memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection tl_reflection)
 
@@ -395,9 +395,9 @@
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
-         is_wfrec(**Lset(i),
-                  iterates_MH(**Lset(i), big_union(**Lset(i)), A),
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
+         is_wfrec(##Lset(i),
+                  iterates_MH(##Lset(i), big_union(##Lset(i)), A),
                   memsn, u, y))]"
 by (intro FOL_reflections function_reflections is_wfrec_reflection
           iterates_MH_reflection)
@@ -419,7 +419,7 @@
    [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
                 is_iterates(L, big_union(L), A, u, x),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
-               is_iterates(**Lset(i), big_union(**Lset(i)), A, u, x)]"
+               is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]"
 by (intro FOL_reflections function_reflections is_iterates_reflection)
 
 lemma eclose_replacement2:
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -32,7 +32,7 @@
 lemma sats_depth_fm [simp]:
    "[| x \<in> nat; y < length(env); env \<in> list(A)|]
     ==> sats(A, depth_fm(x,y), env) <->
-        is_depth(**A, nth(x,env), nth(y,env))"
+        is_depth(##A, nth(x,env), nth(y,env))"
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: depth_fm_def is_depth_def) 
 done
@@ -40,12 +40,12 @@
 lemma depth_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j < length(env); env \<in> list(A)|]
-       ==> is_depth(**A, x, y) <-> sats(A, depth_fm(i,j), env)"
+       ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i,j), env)"
 by (simp add: sats_depth_fm)
 
 theorem depth_reflection:
      "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
-               \<lambda>i x. is_depth(**Lset(i), f(x), g(x))]"
+               \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
 apply (simp only: is_depth_def)
 apply (intro FOL_reflections function_reflections formula_N_reflection) 
 done
@@ -111,7 +111,7 @@
   shows 
       "[|x \<in> nat; y < length(env); env \<in> list(A)|]
        ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
-           is_formula_case(**A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
+           is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: formula_case_fm_def is_formula_case_def 
                  is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
@@ -138,7 +138,7 @@
   shows 
       "[|nth(i,env) = x; nth(j,env) = y; 
       i \<in> nat; j < length(env); env \<in> list(A)|]
-       ==> is_formula_case(**A, ISA, ISB, ISC, ISD, x, y) <->
+       ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
            sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
 by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 
                                        is_c_iff_sats is_d_iff_sats])
@@ -150,18 +150,18 @@
 theorem is_formula_case_reflection:
   assumes is_a_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
-                     \<lambda>i x. is_a(**Lset(i), h(x), f(x), g(x), g'(x))]"
+                     \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_b_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
-                     \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x), g'(x))]"
+                     \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_c_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
-                     \<lambda>i x. is_c(**Lset(i), h(x), f(x), g(x), g'(x))]"
+                     \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
   and is_d_reflection:
     "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
-                     \<lambda>i x. is_d(**Lset(i), h(x), f(x), g(x))]"
+                     \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
   shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
-               \<lambda>i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]"
+               \<lambda>i x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]"
 apply (simp (no_asm_use) only: is_formula_case_def)
 apply (intro FOL_reflections function_reflections finite_ordinal_reflection
          mem_formula_reflection
@@ -518,18 +518,18 @@
 lemma sats_depth_apply_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, depth_apply_fm(x,y,z), env) <->
-        is_depth_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
+        is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
 by (simp add: depth_apply_fm_def is_depth_apply_def)
 
 lemma depth_apply_iff_sats:
     "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
         i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-     ==> is_depth_apply(**A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
+     ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
 by simp
 
 lemma depth_apply_reflection:
      "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
-               \<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
+               \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: is_depth_apply_def)
 apply (intro FOL_reflections function_reflections depth_reflection 
              finite_ordinal_reflection)
@@ -565,7 +565,7 @@
 lemma sats_satisfies_is_a_fm [simp]:
    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
-        satisfies_is_a(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+        satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=x in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm 
@@ -575,13 +575,13 @@
 lemma satisfies_is_a_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
-   ==> satisfies_is_a(**A,nu,nx,ny,nz) <->
+   ==> satisfies_is_a(##A,nu,nx,ny,nz) <->
        sats(A, satisfies_is_a_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_a_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
-               \<lambda>i x. satisfies_is_a(**Lset(i),f(x),g(x),h(x),g'(x))]"
+               \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_a_def) 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
@@ -613,7 +613,7 @@
 lemma sats_satisfies_is_b_fm [simp]:
    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
-        satisfies_is_b(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
+        satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
 apply (frule_tac x=x in lt_length_in_nat, assumption)  
 apply (frule_tac x=y in lt_length_in_nat, assumption)  
 apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm 
@@ -623,13 +623,13 @@
 lemma satisfies_is_b_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
-   ==> satisfies_is_b(**A,nu,nx,ny,nz) <->
+   ==> satisfies_is_b(##A,nu,nx,ny,nz) <->
        sats(A, satisfies_is_b_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_b_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
-               \<lambda>i x. satisfies_is_b(**Lset(i),f(x),g(x),h(x),g'(x))]"
+               \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_b_def) 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
@@ -665,7 +665,7 @@
 lemma sats_satisfies_is_c_fm [simp]:
    "[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
-        satisfies_is_c(**A, nth(u,env), nth(v,env), nth(x,env), 
+        satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env), 
                             nth(y,env), nth(z,env))"  
 by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
 
@@ -673,13 +673,13 @@
   "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny; 
       nth(z,env) = nz;
       u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
-   ==> satisfies_is_c(**A,nu,nv,nx,ny,nz) <->
+   ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) <->
        sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
 by simp
 
 theorem satisfies_is_c_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
-               \<lambda>i x. satisfies_is_c(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
+               \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
 apply (unfold satisfies_is_c_def) 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
@@ -721,20 +721,20 @@
 lemma sats_satisfies_is_d_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
-        satisfies_is_d(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
+        satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
 by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
               sats_bool_of_o_fm)
 
 lemma satisfies_is_d_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
-   ==> satisfies_is_d(**A,nu,nx,ny,nz) <->
+   ==> satisfies_is_d(##A,nu,nx,ny,nz) <->
        sats(A, satisfies_is_d_fm(u,x,y,z), env)"
 by simp
 
 theorem satisfies_is_d_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
-               \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
+               \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_is_d_def) 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
@@ -773,14 +773,14 @@
 lemma sats_satisfies_MH_fm [simp]:
    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
-        satisfies_MH(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
+        satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
 by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
               sats_formula_case_fm)
 
 lemma satisfies_MH_iff_sats:
   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
-   ==> satisfies_MH(**A,nu,nx,ny,nz) <->
+   ==> satisfies_MH(##A,nu,nx,ny,nz) <->
        sats(A, satisfies_MH_fm(u,x,y,z), env)"
 by simp 
 
@@ -792,7 +792,7 @@
 
 theorem satisfies_MH_reflection:
      "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
-               \<lambda>i x. satisfies_MH(**Lset(i),f(x),g(x),h(x),g'(x))]"
+               \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
 apply (unfold satisfies_MH_def) 
 apply (intro FOL_reflections satisfies_reflections)
 done
@@ -808,9 +808,9 @@
           v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
           is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
-             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
-             is_nth(**Lset(i), y, v, ny) \<and>
-          is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
+             is_nth(##Lset(i), y, v, ny) \<and>
+          is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
 by (intro FOL_reflections function_reflections nth_reflection 
           bool_of_o_reflection)
 
@@ -838,9 +838,9 @@
           v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
           is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
-             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
-             is_nth(**Lset(i), y, v, ny) \<and>
-          is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
+             is_nth(##Lset(i), y, v, ny) \<and>
+          is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
 by (intro FOL_reflections function_reflections nth_reflection 
           bool_of_o_reflection)
 
@@ -870,9 +870,9 @@
 		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
      (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
-       fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and>
-       is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and>
-       u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]"
+       fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
+       is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
+       u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
 apply (unfold is_and_def is_not_def) 
 apply (intro FOL_reflections function_reflections)
 done
@@ -903,11 +903,11 @@
                 number1(L,rpco),
                            bo) \<and> pair(L,u,bo,x)),
  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
-        is_bool_of_o (**Lset(i),
+        is_bool_of_o (##Lset(i),
  \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
-	    is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow> 
-	    number1(**Lset(i),rpco),
-		       bo) \<and> pair(**Lset(i),u,bo,x))]"
+	    is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
+	    number1(##Lset(i),rpco),
+		       bo) \<and> pair(##Lset(i),u,bo,x))]"
 apply (unfold is_bool_of_o_def) 
 apply (intro FOL_reflections function_reflections Cons_reflection)
 done
@@ -936,8 +936,8 @@
 lemma formula_rec_replacement_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
              is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
-             is_wfrec (**Lset(i), satisfies_MH(**Lset(i),A), mesa, u, y))]"
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
+             is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
 by (intro FOL_reflections function_reflections satisfies_MH_reflection 
           is_wfrec_reflection) 
 
@@ -965,13 +965,13 @@
 	   satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
 	   u, c) &
 	 pair(L,u,c,x)),
-  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(**Lset(i),u) &
+  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) &
      (\<exists>c \<in> Lset(i).
 	 is_formula_case
-	  (**Lset(i), satisfies_is_a(**Lset(i),A), satisfies_is_b(**Lset(i),A),
-	   satisfies_is_c(**Lset(i),A,g), satisfies_is_d(**Lset(i),A,g),
+	  (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
+	   satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
 	   u, c) &
-	 pair(**Lset(i),u,c,x))]"
+	 pair(##Lset(i),u,c,x))]"
 by (intro FOL_reflections function_reflections mem_formula_reflection
           is_formula_case_reflection satisfies_is_a_reflection
           satisfies_is_b_reflection satisfies_is_c_reflection
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/Constructible/Separation.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -121,7 +121,7 @@
 lemma cartprod_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
                 \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
-                                   pair(**Lset(i),x,y,z))]"
+                                   pair(##Lset(i),x,y,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma cartprod_separation:
@@ -136,7 +136,7 @@
 
 lemma image_Reflects:
      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
-           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
+           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(##Lset(i),x,y,p))]"
 by (intro FOL_reflections function_reflections)
 
 lemma image_separation:
@@ -153,7 +153,7 @@
 lemma converse_Reflects:
   "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
      \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
-                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
+                     pair(##Lset(i),x,y,p) & pair(##Lset(i),y,x,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma converse_separation:
@@ -169,7 +169,7 @@
 
 lemma restrict_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
-        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
+        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(##Lset(i),x,y,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma restrict_separation:
@@ -187,8 +187,8 @@
                   pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
                   xy\<in>s & yz\<in>r,
         \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
-                  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
-                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
+                  pair(##Lset(i),x,z,xz) & pair(##Lset(i),x,y,xy) &
+                  pair(##Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
 by (intro FOL_reflections function_reflections)
 
 lemma comp_separation:
@@ -210,7 +210,7 @@
 
 lemma pred_Reflects:
      "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
-                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
+                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(##Lset(i),y,x,p)]"
 by (intro FOL_reflections function_reflections)
 
 lemma pred_separation:
@@ -225,7 +225,7 @@
 
 lemma Memrel_Reflects:
      "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
-            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
+            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(##Lset(i),x,y,z) & x \<in> y]"
 by (intro FOL_reflections function_reflections)
 
 lemma Memrel_separation:
@@ -244,8 +244,8 @@
             upair(L,cnbf,cnbf,z)),
         \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
               \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
-                pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
-                is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
+                pair(##Lset(i),f,b,p) & pair(##Lset(i),n,b,nb) &
+                is_cons(##Lset(i),nb,f,cnbf) & upair(##Lset(i),cnbf,cnbf,z))]"
 by (intro FOL_reflections function_reflections)
 
 lemma funspace_succ_replacement:
@@ -269,9 +269,9 @@
                 (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
                                    fx \<noteq> gx),
    \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
-          pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
-                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) &
-                  fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
+          pair(##Lset(i),x,a,xa) & xa \<in> r & pair(##Lset(i),x,b,xb) & xb \<in> r &
+                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(##Lset(i),f,x,fx) &
+                  fun_apply(##Lset(i),g,x,gx) & fx \<noteq> gx)]"
 by (intro FOL_reflections function_reflections fun_plus_reflections)
 
 lemma is_recfun_separation:
diff -r fd40c9d9076b -r a28a8fbc76d4 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Feb 06 11:01:05 2003 +0100
@@ -333,16 +333,16 @@
 
 subsubsection{*Sets as Classes*}
 
-constdefs setclass :: "[i,i] => o"       ("**_" [40] 40)
+constdefs setclass :: "[i,i] => o"       ("##_" [40] 40)
    "setclass(A) == %x. x : A"
 
 lemma setclass_iff [simp]: "setclass(A,x) <-> x : A"
 by (simp add: setclass_def)
 
-lemma rall_setclass_is_ball [simp]: "(\<forall>x[**A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
+lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
 by auto
 
-lemma rex_setclass_is_bex [simp]: "(\<exists>x[**A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
+lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
 by auto