diff -r 69d815b0e1eb -r 21291189b51e univ.ML
--- a/univ.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/univ.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -123,7 +123,7 @@
 
 (** Scons vs Atom **)
 
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M$N) ~= Atom(a)";
 by (rtac notI 1);
 by (etac (equalityD2 RS subsetD RS UnE) 1);
 by (rtac singletonI 1);
@@ -182,30 +182,30 @@
 
 (** Injectiveness of Scons **)
 
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> M<=M'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
 by (cut_facts_tac [major] 1);
 by (fast_tac (set_cs addSDs [Suc_inject]
 		     addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
 val Scons_inject_lemma1 = result();
 
-val [major] = goalw Univ.thy [Scons_def] "M.N <= M'.N' ==> N<=N'";
+val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
 by (cut_facts_tac [major] 1);
 by (fast_tac (set_cs addSDs [Suc_inject]
 		     addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
 val Scons_inject_lemma2 = result();
 
-val [major] = goal Univ.thy "M.N = M'.N' ==> M=M'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
 val Scons_inject1 = result();
 
-val [major] = goal Univ.thy "M.N = M'.N' ==> N=N'";
+val [major] = goal Univ.thy "M$N = M'$N' ==> N=N'";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
 val Scons_inject2 = result();
 
 val [major,minor] = goal Univ.thy
-    "[| M.N = M'.N';  [| M=M';  N=N' |] ==> P \
+    "[| M$N = M'$N';  [| M=M';  N=N' |] ==> P \
 \    |] ==> P";
 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
 val Scons_inject = result();
@@ -215,7 +215,7 @@
 by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
 val Atom_Atom_eq = result();
 
-goal Univ.thy "(M.N = M'.N') = (M=M' & N=N')";
+goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
 by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
 val Scons_Scons_eq = result();
 
@@ -223,7 +223,7 @@
 
 (** Scons vs Leaf **)
 
-goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
+goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
 by (stac o_def 1);
 by (rtac Scons_not_Atom 1);
 val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
 
 (** Scons vs Numb **)
 
-goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
+goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
 by (stac o_def 1);
 by (rtac Scons_not_Atom 1);
 val Scons_not_Numb = result();
@@ -312,7 +312,7 @@
 val ntrunc_Numb = result();
 
 goalw Univ.thy [Scons_def,ntrunc_def]
-    "ntrunc(Suc(k), M.N) = ntrunc(k,M) . ntrunc(k,N)";
+    "ntrunc(Suc(k), M$N) = ntrunc(k,M) $ ntrunc(k,N)";
 by (safe_tac (set_cs addSIs [equalityI,imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
@@ -347,14 +347,14 @@
 
 (*** Cartesian Product ***)
 
-goalw Univ.thy [uprod_def] "!!M N. [| M:A;  N:B |] ==> (M.N) : A<*>B";
+goalw Univ.thy [uprod_def] "!!M N. [| M:A;  N:B |] ==> (M$N) : A<*>B";
 by (REPEAT (ares_tac [singletonI,UN_I] 1));
 val uprodI = result();
 
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [uprod_def]
     "[| c : A<*>B;  \
-\       !!x y. [| x:A;  y:B;  c=x.y |] ==> P \
+\       !!x y. [| x:A;  y:B;  c=x$y |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
@@ -363,7 +363,7 @@
 
 (*Elimination of a pair -- introduces no eigenvariables*)
 val prems = goal Univ.thy
-    "[| (M.N) : A<*>B;      [| M:A;  N:B |] ==> P   \
+    "[| (M$N) : A<*>B;      [| M:A;  N:B |] ==> P   \
 \    |] ==> P";
 by (rtac uprodE 1);
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
@@ -448,7 +448,7 @@
 by (fast_tac set_cs 1);
 val usum_mono = result();
 
-goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M.N <= M'.N'";
+goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
 by (fast_tac set_cs 1);
 val Scons_mono = result();
 
@@ -463,7 +463,7 @@
 
 (*** Split and Case ***)
 
-goalw Univ.thy [Split_def] "Split(M.N, c) = c(M,N)";
+goalw Univ.thy [Split_def] "Split(M$N, c) = c(M,N)";
 by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
 val Split = result();
 
@@ -483,11 +483,11 @@
 by (fast_tac (set_cs addIs [equalityI]) 1);
 val ntrunc_UN1 = result();
 
-goalw Univ.thy [Scons_def] "(UN x.f(x)) . M = (UN x. f(x) . M)";
+goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
 by (fast_tac (set_cs addIs [equalityI]) 1);
 val Scons_UN1_x = result();
 
-goalw Univ.thy [Scons_def] "M . (UN x.f(x)) = (UN x. M . f(x))";
+goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
 by (fast_tac (set_cs addIs [equalityI]) 1);
 val Scons_UN1_y = result();
 
@@ -518,12 +518,12 @@
 (*** Equality for Cartesian Product ***)
 
 goal Univ.thy
- "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x.y,x'.y'>})) = {<M.N, M'.N'>}";
+ "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x$y,x'$y'>})) = {<M$N, M'$N'>}";
 by (simp_tac univ_ss 1);
 val dprod_lemma = result();
 
 goalw Univ.thy [dprod_def]
-    "!!r s. [| <M,M'>:r;  <N,N'>:s |] ==> <M.N, M'.N'> : r<**>s";
+    "!!r s. [| <M,M'>:r;  <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
 by (REPEAT (ares_tac [UN_I] 1));
 by (rtac (singletonI RS (dprod_lemma RS equalityD2 RS subsetD)) 1);
 val dprodI = result();
@@ -531,7 +531,7 @@
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [dprod_def]
     "[| c : r<**>s;  \
-\       !!x y x' y'. [| <x,x'> : r;  <y,y'> : s;  c = <x.y,x'.y'> |] ==> P \
+\       !!x y x' y'. [| <x,x'> : r;  <y,y'> : s;  c = <x$y,x'$y'> |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1));