# HG changeset patch
# User clasohm
# Date 762607615 -3600
# Node ID 21291189b51e614f8c493f0595e6981b46d3573a
# Parent  69d815b0e1ebd5e9a9304fde5a9a07f5d00020cf
changed "." to "$" and Cons to infix "#" to eliminate ambiguity

diff -r 69d815b0e1eb -r 21291189b51e HOL.ML
--- a/HOL.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/HOL.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -337,6 +337,7 @@
 fun sstac ths = EVERY' (map stac ths);
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
+
 end;
 
 open HOL_Lemmas;
diff -r 69d815b0e1eb -r 21291189b51e List.ML
--- a/List.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/List.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -52,7 +52,7 @@
 (*Induction for the type 'a list *)
 val prems = goalw List.thy [Nil_def,Cons_def]
     "[| P(Nil);   \
-\       !!x xs. P(xs) ==> P(Cons(x,xs)) |]  ==> P(l)";
+\       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
 by (rtac (Rep_List_inverse RS subst) 1);   (*types force good instantiation*)
 by (rtac (Rep_List RS List_induct) 1);
 by (REPEAT (ares_tac prems 1
@@ -104,7 +104,7 @@
 val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
-goalw List.thy [Nil_def,Cons_def] "Cons(x,xs) ~= Nil";
+goalw List.thy [Nil_def,Cons_def] "x # xs ~= Nil";
 by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
 val Cons_not_Nil = result();
@@ -128,7 +128,7 @@
 		     addSDs [inj_onto_Abs_List RS inj_ontoD,
 			     inj_Rep_List RS injD, Leaf_inject];
 
-goalw List.thy [Cons_def] "(Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)";
+goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
 by (fast_tac List_cs 1);
 val Cons_Cons_eq = result();
 val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
@@ -157,13 +157,13 @@
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_CONS_self = result();
 
-goal List.thy "!x. l ~= Cons(x,l)";
+goal List.thy "!x. l ~= x#l";
 by (list_ind_tac "l" 1);
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_Cons_self = result();
 
 
-goal List.thy "(xs ~= []) = (? y ys. xs = Cons(y,ys))";
+goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
 by(list_ind_tac "xs" 1);
 by(simp_tac list_free_ss 1);
 by(asm_simp_tac list_free_ss 1);
@@ -240,7 +240,7 @@
    (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
 
   val list_rec_Cons = prove_goalw List.thy [list_rec_def, Cons_def]
-      "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"
+      "list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))"
    (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
 end;
 
@@ -269,7 +269,7 @@
 val Rep_map_Nil = result();
 
 goalw List.thy [Rep_map_def]
-    "Rep_map(f, Cons(x,xs)) = CONS(f(x), Rep_map(f,xs))";
+    "Rep_map(f, x#xs) = CONS(f(x), Rep_map(f,xs))";
 by (rtac list_rec_Cons 1);
 val Rep_map_Cons = result();
 
@@ -284,7 +284,7 @@
 
 val prems = goalw List.thy [Abs_map_def]
     "[| M: Sexp;  N: Sexp |] ==> \
-\    Abs_map(g, CONS(M,N)) = Cons(g(M), Abs_map(g,N))";
+\    Abs_map(g, CONS(M,N)) = g(M) # Abs_map(g,N)";
 by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
 val Abs_map_CONS = result();
 
@@ -296,7 +296,7 @@
 val def_list_rec_Nil = result();
 
 val [rew] = goal List.thy
-    "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(Cons(x,xs)) = h(x,xs,f(xs))";
+    "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(x#xs) = h(x,xs,f(xs))";
 by (rewtac rew);
 by (rtac list_rec_Cons 1);
 val def_list_rec_Cons = result();
@@ -393,7 +393,7 @@
 
 goal List.thy
  "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
-\                         (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
+\                         (!y ys. xs=y#ys --> P(f(y,ys))))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac list_ss));
 by(fast_tac HOL_cs 1);
diff -r 69d815b0e1eb -r 21291189b51e List.thy
--- a/List.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/List.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -28,7 +28,7 @@
   NIL           :: "'a node set"
   CONS          :: "['a node set, 'a node set] => 'a node set"
   Nil           :: "'a list"
-  Cons          :: "['a, 'a list] => 'a list"
+  "#"           :: "['a, 'a list] => 'a list"                   (infixr 65)
   List_case     :: "['a node set, 'b, ['a node set, 'a node set]=>'b] => 'b"
   List_rec      :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
   list_rec      :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
@@ -40,7 +40,7 @@
   mem		:: "['a, 'a list] => bool"			(infixl 55)
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
-  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
+  "@"		:: "['a list, 'a list] => 'a list"		(infixl 65)
   list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
   filter	:: "['a => bool, 'a list] => 'a list"
 
@@ -54,11 +54,11 @@
   "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
 
 translations
-  "[x, xs]"     == "Cons(x, [xs])"
-  "[x]"         == "Cons(x, [])"
+  "[x, xs]"     == "x#[xs]"
+  "[x]"         == "x#[]"
   "[]"          == "Nil"
 
-  "case xs of Nil => a | Cons(y,ys) => b" == "list_case(xs,a,%y ys.b)"
+  "case xs of Nil => a | y#ys => b" == "list_case(xs,a,%y ys.b)"
 
   "[x:xs . P]"	== "filter(%x.P,xs)"
   "Alls x:xs.P"	== "list_all(%x.P,xs)"
@@ -77,12 +77,12 @@
   (* Defining the Concrete Constructors *)
 
   NIL_def       "NIL == In0(Numb(0))"
-  CONS_def      "CONS(M, N) == In1(M . N)"
+  CONS_def      "CONS(M, N) == In1(M $ N)"
 
   (* Defining the Abstract Constructors *)
 
   Nil_def       "Nil == Abs_List(NIL)"
-  Cons_def      "Cons(x, xs) == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
+  Cons_def      "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
 
   List_case_def "List_case(M, c, d) == Case(M, %x.c, %u. Split(u, %x y.d(x, y)))"
 
@@ -101,7 +101,7 @@
   Rep_map_def
    "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))"
   Abs_map_def
-   "Abs_map(g, M) == List_rec(M, Nil, %N L r. Cons(g(N), r))"
+   "Abs_map(g, M) == List_rec(M, Nil, %N L r. g(N)#r)"
 
   null_def      "null(xs)            == list_rec(xs, True, %x xs r.False)"
   hd_def        "hd(xs)              == list_rec(xs, @x.True, %x xs r.x)"
@@ -111,10 +111,10 @@
   mem_def	"x mem xs            == \
 \		   list_rec(xs, False, %y ys r. if(y=x, True, r))"
   list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
-  map_def       "map(f, xs)          == list_rec(xs, [], %x l r. Cons(f(x),r))"
-  append_def	"xs@ys               == list_rec(xs, ys, %x l r. Cons(x,r))"
+  map_def       "map(f, xs)          == list_rec(xs, [], %x l r. f(x)#r)"
+  append_def	"xs@ys               == list_rec(xs, ys, %x l r. x#r)"
   filter_def	"filter(P,xs)        == \
-\                  list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
+\                  list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
   list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end
diff -r 69d815b0e1eb -r 21291189b51e Sexp.ML
--- a/Sexp.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Sexp.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -20,7 +20,7 @@
 
 val major::prems = goal Sexp.thy 
     "[| ii: Sexp;  !!a. P(Leaf(a));   !!k. P(Numb(k));   \
-\       !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i.j) \
+\       !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \
 \    |]  ==> P(ii)";
 by (rtac (major RS (Sexp_def RS def_induct)) 1);
 by (rtac Sexp_fun_mono 1);
@@ -41,7 +41,7 @@
 		     addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
 val Sexp_case_Numb = result();
 
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M.N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
 by (fast_tac (HOL_cs addIs  [select_equality] 
 	             addSDs [Scons_inject]
 	             addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
@@ -61,7 +61,7 @@
 val Sexp_NumbI = result();
 
 val prems = goal Sexp.thy 
-    "[| M: Sexp;  N: Sexp |] ==> M.N : Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> M$N : Sexp";
 by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
 val Sexp_SconsI = result();
 
@@ -79,7 +79,7 @@
 by (fast_tac (set_cs addIs [SexpI]) 1);
 val range_Leaf_subset_Sexp = result();
 
-val [major] = goal Sexp.thy "M.N : Sexp ==> M: Sexp & N: Sexp";
+val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac Sexp_induct 1);
 by (ALLGOALS 
@@ -101,12 +101,12 @@
     pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
 
 val prems = goalw Sexp.thy [pred_Sexp_def]
-    "[| M: Sexp;  N: Sexp |] ==> <M, M.N> : pred_Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> <M, M$N> : pred_Sexp";
 by (fast_tac (set_cs addIs prems) 1);
 val pred_SexpI1 = result();
 
 val prems = goalw Sexp.thy [pred_Sexp_def]
-    "[| M: Sexp;  N: Sexp |] ==> <N, M.N> : pred_Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> <N, M$N> : pred_Sexp";
 by (fast_tac (set_cs addIs prems) 1);
 val pred_SexpI2 = result();
 
@@ -126,8 +126,8 @@
 
 val major::prems = goalw Sexp.thy [pred_Sexp_def]
     "[| p : pred_Sexp;  \
-\       !!M N. [| p = <M, M.N>;  M: Sexp;  N: Sexp |] ==> R; \
-\       !!M N. [| p = <N, M.N>;  M: Sexp;  N: Sexp |] ==> R  \
+\       !!M N. [| p = <M, M$N>;  M: Sexp;  N: Sexp |] ==> R; \
+\       !!M N. [| p = <N, M$N>;  M: Sexp;  N: Sexp |] ==> R  \
 \    |] ==> R";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
@@ -159,7 +159,7 @@
 val Sexp_rec_Numb = result();
 
 goal Sexp.thy "!!M. [| M: Sexp;  N: Sexp |] ==> \
-\    Sexp_rec(M.N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
+\    Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
 by (rtac (Sexp_rec_unfold RS trans) 1);
 by (asm_simp_tac(HOL_ss addsimps
                [Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
diff -r 69d815b0e1eb -r 21291189b51e Sexp.thy
--- a/Sexp.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Sexp.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -24,10 +24,10 @@
   Sexp_case_def	
    "Sexp_case(M,c,d,e) == @ z. (? x.   M=Leaf(x) & z=c(x))  \
 \                            | (? k.   M=Numb(k) & z=d(k))  \
-\                            | (? N1 N2. M = N1 . N2  & z=e(N1,N2))"
+\                            | (? N1 N2. M = N1 $ N2  & z=e(N1,N2))"
 
   pred_Sexp_def
-     "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M.N>, <N, M.N>}"
+     "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}"
 
   Sexp_rec_def
    "Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M,  \
diff -r 69d815b0e1eb -r 21291189b51e Subst/AList.ML
--- a/Subst/AList.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/AList.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,15 +19,15 @@
                             (fn _ => [simp_tac alist_ss 1])
   in map mk_thm 
      ["alist_rec(Nil,c,d) = c",
-      "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
+      "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
       "assoc(v,d,Nil) = d",
-      "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;
+      "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
 
 (*********)
 
 val prems = goal AList.thy
     "[| P(Nil);   \
-\       !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |]  ==> P(l)";
+\       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
 by (list_ind_tac "l" 1);
 by (resolve_tac prems 1);
 by (rtac PairE 1);
@@ -43,7 +43,7 @@
 
 (*
 val prems = goal AList.thy
-    "[| P(Nil);  !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
+    "[| P(Nil);  !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
 by (alist_ind_tac "a" 1);
 by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
 val alist_induct2 = result();
diff -r 69d815b0e1eb -r 21291189b51e Subst/ROOT.ML
--- a/Subst/ROOT.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/ROOT.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,12 +19,13 @@
 unifier      -  specification of unification and conditions for 
                 correctness and termination
 
-To load, go to the parent directory and type use"Substitutions/ROOT.ML";
+To load, go to the parent directory and type use"Subst/ROOT.ML";
 *)
 
 HOL_build_completed;    (*Cause examples to fail if HOL did*)
 
 writeln"Root file for Substitutions and Unification";
+loadpath := ["Subst"];
 use_thy "Subst/Setplus";
 
 use_thy "Subst/AList";
diff -r 69d815b0e1eb -r 21291189b51e Subst/Subst.ML
--- a/Subst/Subst.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Subst.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,9 +19,9 @@
 ["Const(c) <| al = Const(c)",
  "Comb(t,u) <| al = Comb(t <| al, u <| al)",
  "Nil <> bl = bl",
- "Cons(<a,b>,al) <> bl = Cons(<a,b <| bl>, al <> bl)",
+ "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
  "sdom(Nil) = {}",
- "sdom(Cons(<a,b>,al)) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
+ "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
 ];
    (* This rewrite isn't always desired *)
    val Var_subst = mk_thm "Var(x) <| al = assoc(x,Var(x),al)";
@@ -41,10 +41,10 @@
 by (ALLGOALS (asm_simp_tac subst_ss));
 val subst_mono = result() RS mp;
 
-goal Subst.thy  "~ (Var(v) <: t) --> t <| Cons(<v,t <| s>,s) = t <| s";
+goal Subst.thy  "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
 by (imp_excluded_middle_tac "t = Var(v)" 1);
 by (res_inst_tac [("P",
-    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| Cons(<v,t<|s>,s)=x<|s")]
+    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
     uterm_induct 2);
 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
 by (fast_tac HOL_cs 1);
@@ -58,13 +58,13 @@
 by (ALLGOALS (fast_tac HOL_cs));
 val agreement = result();
 
-goal Subst.thy   "~ v: vars_of(t) --> t <| Cons(<v,u>,s) = t <| s";
+goal Subst.thy   "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
 by(simp_tac(subst_ss addsimps [agreement,Var_subst]
                      setloop (split_tac [expand_if])) 1);
 val repl_invariance = result() RS mp;
 
 val asms = goal Subst.thy 
-     "v : vars_of(t) --> w : vars_of(t <| Cons(<v,Var(w)>,s))";
+     "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
 val Var_in_subst = result() RS mp;
@@ -112,7 +112,7 @@
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
 val comp_assoc = result();
 
-goal Subst.thy "Cons(<w,Var(w) <| s>,s) =s= s"; 
+goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
 by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
 by (uterm_ind_tac "t" 1);
 by (REPEAT (etac rev_mp 3));
diff -r 69d815b0e1eb -r 21291189b51e Subst/Subst.thy
--- a/Subst/Subst.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Subst.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -26,7 +26,7 @@
 \                          %x.Const(x),			\
 \                          %u v q r.Comb(q,r))"
 
-  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.Cons(<x,y <| bl>,g))"
+  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
 
   sdom_def
   "sdom(al) == alist_rec(al, {},  \
diff -r 69d815b0e1eb -r 21291189b51e Subst/UTerm.thy
--- a/Subst/UTerm.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/UTerm.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -37,7 +37,7 @@
      (*defining the concrete constructors*)
   VAR_def  	"VAR(v) == In0(v)"
   CONST_def  	"CONST(v) == In1(In0(v))"
-  COMB_def 	"COMB(t,u) == In1(In1(t . u))"
+  COMB_def 	"COMB(t,u) == In1(In1(t $ u))"
      (*defining the abstract constructors*)
   Var_def  	"Var(v) == Abs_UTerm(VAR(Leaf(v)))"
   Const_def  	"Const(c) == Abs_UTerm(CONST(Leaf(c)))"
diff -r 69d815b0e1eb -r 21291189b51e Subst/Unifier.ML
--- a/Subst/Unifier.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/Unifier.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -25,7 +25,7 @@
 
 goal Unifier.thy
   "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
-\  Unifier(Cons(<v,r>,s),t,u)";
+\  Unifier(<v,r>#s,t,u)";
 by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
 val Cons_Unifier = result() RS mp RS mp RS mp;
 
@@ -49,7 +49,7 @@
 val MGU_iff = result();
 
 val [prem] = goal Unifier.thy
-     "~ Var(v) <: t ==> MGUnifier(Cons(<v,t>,Nil),Var(v),t)";
+     "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
 by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
 by (REPEAT_SOME (step_tac set_cs));
 by (etac subst 1);
@@ -85,7 +85,7 @@
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
 val Idem_Nil = result();
 
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(Cons(<v,t>,Nil))";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
 by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
                        setloop (split_tac [expand_if])) 1);
 by (fast_tac set_cs 1);
@@ -114,8 +114,8 @@
 
 val prems = goal Unifier.thy 
     "x : sdom(s) -->  ~x : srange(s) --> \
-\   ~vars_of(Var(x) <| s<>Cons(<x,Var(x)>,s)) = \
-\      vars_of(Var(x) <| Cons(<x,Var(x)>,s))";
+\   ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\      vars_of(Var(x) <| <x,Var(x)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI2] 1));
 by(res_inst_tac [("x","x")] exI 1);
@@ -141,8 +141,8 @@
 
 val prems = goal Unifier.thy 
    "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\   ~vars_of(Var(w) <| s<>Cons(<x,Var(w)>,s)) = \
-\   vars_of(Var(w) <| Cons(<x,Var(w)>,s))";
+\   ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\   vars_of(Var(w) <| <x,Var(w)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI1] 1));
 by(res_inst_tac [("x","w")] exI 1);
@@ -167,10 +167,10 @@
 (*                                                                           *)
 (*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
 (*    | unify Const(m) _        = Fail                                       *)
-(*    | unify Var(v)   t        = if Var(v)<:t then Fail else Cons(<v,t>,Nil)*)
+(*    | unify Var(v)   t        = if Var(v)<:t then Fail else <v,t>#Nil      *)
 (*    | unify Comb(t,u) Const(n) = Fail                                      *)
 (*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
-(*                                               else Cons(<v,Comb(t,u>,Nil) *)
+(*                                               else <v,Comb(t,u>#Nil       *)
 (*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
 (*                                  in if s=Fail then Fail                   *)
 (*                                               else unify (u<|s) (w<|s);   *)
@@ -191,7 +191,7 @@
 val Unify2 = result() RS mp;
 
 val [prem] = goalw Unifier.thy [MGIUnifier_def] 
- "~Var(v) <: t ==> MGIUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
 by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
 val Unify3 = result();
 
diff -r 69d815b0e1eb -r 21291189b51e Subst/alist.ML
--- a/Subst/alist.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/alist.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,15 +19,15 @@
                             (fn _ => [simp_tac alist_ss 1])
   in map mk_thm 
      ["alist_rec(Nil,c,d) = c",
-      "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
+      "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
       "assoc(v,d,Nil) = d",
-      "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;
+      "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
 
 (*********)
 
 val prems = goal AList.thy
     "[| P(Nil);   \
-\       !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |]  ==> P(l)";
+\       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
 by (list_ind_tac "l" 1);
 by (resolve_tac prems 1);
 by (rtac PairE 1);
@@ -43,7 +43,7 @@
 
 (*
 val prems = goal AList.thy
-    "[| P(Nil);  !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
+    "[| P(Nil);  !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
 by (alist_ind_tac "a" 1);
 by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
 val alist_induct2 = result();
diff -r 69d815b0e1eb -r 21291189b51e Subst/subst.ML
--- a/Subst/subst.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/subst.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,9 +19,9 @@
 ["Const(c) <| al = Const(c)",
  "Comb(t,u) <| al = Comb(t <| al, u <| al)",
  "Nil <> bl = bl",
- "Cons(<a,b>,al) <> bl = Cons(<a,b <| bl>, al <> bl)",
+ "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
  "sdom(Nil) = {}",
- "sdom(Cons(<a,b>,al)) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
+ "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
 ];
    (* This rewrite isn't always desired *)
    val Var_subst = mk_thm "Var(x) <| al = assoc(x,Var(x),al)";
@@ -41,10 +41,10 @@
 by (ALLGOALS (asm_simp_tac subst_ss));
 val subst_mono = result() RS mp;
 
-goal Subst.thy  "~ (Var(v) <: t) --> t <| Cons(<v,t <| s>,s) = t <| s";
+goal Subst.thy  "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
 by (imp_excluded_middle_tac "t = Var(v)" 1);
 by (res_inst_tac [("P",
-    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| Cons(<v,t<|s>,s)=x<|s")]
+    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
     uterm_induct 2);
 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
 by (fast_tac HOL_cs 1);
@@ -58,13 +58,13 @@
 by (ALLGOALS (fast_tac HOL_cs));
 val agreement = result();
 
-goal Subst.thy   "~ v: vars_of(t) --> t <| Cons(<v,u>,s) = t <| s";
+goal Subst.thy   "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
 by(simp_tac(subst_ss addsimps [agreement,Var_subst]
                      setloop (split_tac [expand_if])) 1);
 val repl_invariance = result() RS mp;
 
 val asms = goal Subst.thy 
-     "v : vars_of(t) --> w : vars_of(t <| Cons(<v,Var(w)>,s))";
+     "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
 val Var_in_subst = result() RS mp;
@@ -112,7 +112,7 @@
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
 val comp_assoc = result();
 
-goal Subst.thy "Cons(<w,Var(w) <| s>,s) =s= s"; 
+goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
 by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
 by (uterm_ind_tac "t" 1);
 by (REPEAT (etac rev_mp 3));
diff -r 69d815b0e1eb -r 21291189b51e Subst/subst.thy
--- a/Subst/subst.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/subst.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -26,7 +26,7 @@
 \                          %x.Const(x),			\
 \                          %u v q r.Comb(q,r))"
 
-  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.Cons(<x,y <| bl>,g))"
+  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
 
   sdom_def
   "sdom(al) == alist_rec(al, {},  \
diff -r 69d815b0e1eb -r 21291189b51e Subst/unifier.ML
--- a/Subst/unifier.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/unifier.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -25,7 +25,7 @@
 
 goal Unifier.thy
   "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
-\  Unifier(Cons(<v,r>,s),t,u)";
+\  Unifier(<v,r>#s,t,u)";
 by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
 val Cons_Unifier = result() RS mp RS mp RS mp;
 
@@ -49,7 +49,7 @@
 val MGU_iff = result();
 
 val [prem] = goal Unifier.thy
-     "~ Var(v) <: t ==> MGUnifier(Cons(<v,t>,Nil),Var(v),t)";
+     "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
 by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
 by (REPEAT_SOME (step_tac set_cs));
 by (etac subst 1);
@@ -85,7 +85,7 @@
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
 val Idem_Nil = result();
 
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(Cons(<v,t>,Nil))";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
 by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
                        setloop (split_tac [expand_if])) 1);
 by (fast_tac set_cs 1);
@@ -114,8 +114,8 @@
 
 val prems = goal Unifier.thy 
     "x : sdom(s) -->  ~x : srange(s) --> \
-\   ~vars_of(Var(x) <| s<>Cons(<x,Var(x)>,s)) = \
-\      vars_of(Var(x) <| Cons(<x,Var(x)>,s))";
+\   ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\      vars_of(Var(x) <| <x,Var(x)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI2] 1));
 by(res_inst_tac [("x","x")] exI 1);
@@ -141,8 +141,8 @@
 
 val prems = goal Unifier.thy 
    "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\   ~vars_of(Var(w) <| s<>Cons(<x,Var(w)>,s)) = \
-\   vars_of(Var(w) <| Cons(<x,Var(w)>,s))";
+\   ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\   vars_of(Var(w) <| <x,Var(w)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI1] 1));
 by(res_inst_tac [("x","w")] exI 1);
@@ -167,10 +167,10 @@
 (*                                                                           *)
 (*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
 (*    | unify Const(m) _        = Fail                                       *)
-(*    | unify Var(v)   t        = if Var(v)<:t then Fail else Cons(<v,t>,Nil)*)
+(*    | unify Var(v)   t        = if Var(v)<:t then Fail else <v,t>#Nil      *)
 (*    | unify Comb(t,u) Const(n) = Fail                                      *)
 (*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
-(*                                               else Cons(<v,Comb(t,u>,Nil) *)
+(*                                               else <v,Comb(t,u>#Nil       *)
 (*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
 (*                                  in if s=Fail then Fail                   *)
 (*                                               else unify (u<|s) (w<|s);   *)
@@ -191,7 +191,7 @@
 val Unify2 = result() RS mp;
 
 val [prem] = goalw Unifier.thy [MGIUnifier_def] 
- "~Var(v) <: t ==> MGIUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
 by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
 val Unify3 = result();
 
diff -r 69d815b0e1eb -r 21291189b51e Subst/uterm.thy
--- a/Subst/uterm.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/uterm.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -37,7 +37,7 @@
      (*defining the concrete constructors*)
   VAR_def  	"VAR(v) == In0(v)"
   CONST_def  	"CONST(v) == In1(In0(v))"
-  COMB_def 	"COMB(t,u) == In1(In1(t . u))"
+  COMB_def 	"COMB(t,u) == In1(In1(t $ u))"
      (*defining the abstract constructors*)
   Var_def  	"Var(v) == Abs_UTerm(VAR(Leaf(v)))"
   Const_def  	"Const(c) == Abs_UTerm(CONST(Leaf(c)))"
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));
diff -r 69d815b0e1eb -r 21291189b51e Univ.thy
--- a/Univ.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/Univ.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -29,7 +29,7 @@
   Atom      :: "('a+nat) => 'a node set"
   Leaf      :: "'a => 'a node set"
   Numb      :: "nat => 'a node set"
-  "."       :: "['a node set, 'a node set]=> 'a node set" 	(infixr 60)
+  "$"       :: "['a node set, 'a node set]=> 'a node set" 	(infixr 60)
   In0,In1   :: "'a node set => 'a node set"
 
   ntrunc    :: "[nat, 'a node set] => 'a node set"
@@ -67,26 +67,26 @@
 
   (*S-expression constructors*)
   Atom_def   "Atom == (%x. {Abs_Node(<%k.0, x>)})"
-  Scons_def  "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+  Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
 
   (*Leaf nodes, with arbitrary or nat labels*)
   Leaf_def   "Leaf == Atom o Inl"
   Numb_def   "Numb == Atom o Inr"
 
   (*Injections of the "disjoint sum"*)
-  In0_def    "In0(M) == Numb(0) . M"
-  In1_def    "In1(M) == Numb(Suc(0)) . M"
+  In0_def    "In0(M) == Numb(0) $ M"
+  In1_def    "In1(M) == Numb(Suc(0)) $ M"
 
   (*the set of nodes with depth less than k*)
   ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
   ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
-  uprod_def  "A<*>B == UN x:A. UN y:B. { (x.y) }"
+  uprod_def  "A<*>B == UN x:A. UN y:B. { (x$y) }"
   usum_def   "A<+>B == In0``A Un In1``B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)"
+  Split_def  "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
 
   Case_def   "Case(M,c,d) == @u.  (? x . M = In0(x) & u = c(x))	\
 \	   	                | (? y . M = In1(y) & u = d(y))"
@@ -97,7 +97,7 @@
   diag_def   "diag(A) == UN x:A. {<x,x>}"
 
   dprod_def  "r<**>s == UN u:r. UN v:s. \
-\                       split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))"
+\                       split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
 
   dsum_def   "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
 \                       (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"
diff -r 69d815b0e1eb -r 21291189b51e ex/InSort.thy
--- a/ex/InSort.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/InSort.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -14,9 +14,9 @@
 
 rules
   ins_Nil  "ins(f,x,[]) = [x]"
-  ins_Cons "ins(f,x,Cons(y,ys)) =   \
-\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+  ins_Cons "ins(f,x,y#ys) =   \
+\	       if(f(x,y), x#y#ys, y# ins(f,x,ys))"
 
   insort_Nil  "insort(f,[]) = []"
-  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+  insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
 end
diff -r 69d815b0e1eb -r 21291189b51e ex/PL.ML
--- a/ex/PL.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/PL.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -158,7 +158,7 @@
 by (simp_tac pl_ss 1);
 val hyps_false = result();
 
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
+goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, (#v)->false)}";
 by (simp_tac pl_ss 1);
 val hyps_var = result();
 
@@ -250,7 +250,7 @@
 
 (*For the case hyps(p,t)-insert(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-goal PL.thy "!p.hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})";
+goal PL.thy "!p.hyps(p, t-{v}) <= insert((#v)->false, hyps(p,t)-{#v})";
 by (rtac pl_ind 1);
 by (simp_tac pl_ss 1);
 by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -260,8 +260,8 @@
 val hyps_Diff = result() RS spec;
 
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
-  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
-goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})";
+  we also have hyps(p,t)-{(#v)->false} <= hyps(p, insert(v,t)) *)
+goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
 by (rtac pl_ind 1);
 by (simp_tac pl_ss 1);
 by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -282,7 +282,7 @@
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
+goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, (#v)->false})";
 by (rtac pl_ind 1);
 by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
               fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
diff -r 69d815b0e1eb -r 21291189b51e ex/PL.thy
--- a/ex/PL.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/PL.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -46,7 +46,7 @@
 eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
 
 hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
 
 var_inject "(#v = #w) ==> v = w"
 imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R"
diff -r 69d815b0e1eb -r 21291189b51e ex/Qsort.thy
--- a/ex/Qsort.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Qsort.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -13,8 +13,8 @@
 rules
 
 qsort_Nil  "qsort(le,[]) = []"
-qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
-\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
+qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\                            (x# qsort(le,[y:xs . le(x,y)]))"
 
 (* computational induction.
    The dependence of p on x but not xs is intentional.
@@ -22,6 +22,6 @@
 qsort_ind
  "[| P([]); \
 \    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
-\            P(Cons(x,xs)) |] \
+\            P(x#xs) |] \
 \ ==> P(xs)"
 end
diff -r 69d815b0e1eb -r 21291189b51e ex/Simult.thy
--- a/ex/Simult.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Simult.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -50,7 +50,7 @@
 	"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
 
      (*the concrete constants*)
-  TCONS_def 	"TCONS(M,N) == In0(M . N)"
+  TCONS_def 	"TCONS(M,N) == In0(M $ N)"
   FNIL_def	"FNIL       == In1(NIL)"
   FCONS_def	"FCONS(M,N) == In1(CONS(M,N))"
      (*the abstract constants*)
diff -r 69d815b0e1eb -r 21291189b51e ex/Sorting.thy
--- a/ex/Sorting.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Sorting.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -18,13 +18,13 @@
 
 sorted1_Nil  "sorted1(f,[])"
 sorted1_One  "sorted1(f,[x])"
-sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
 
 sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
 
 mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
 
 total_def  "total(r) == (!x y. r(x,y) | r(y,x))"
 transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))"
diff -r 69d815b0e1eb -r 21291189b51e ex/Term.ML
--- a/ex/Term.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Term.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -40,7 +40,7 @@
 val [major,minor] = goal Term.thy 
     "[| M: Term(A);  \
 \       !!x zs. [| x: A;  zs: List(Term(A));  zs: List({x.R(x)}) \
-\               |] ==> R(x.zs)  \
+\               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS (Term_def RS def_induct)) 1);
 by (rtac Term_fun_mono 1);
@@ -51,9 +51,9 @@
 (*Induction on Term(A) followed by induction on List *)
 val major::prems = goal Term.thy
     "[| M: Term(A);  \
-\       !!x.      [| x: A |] ==> R(x.NIL);  \
-\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x.zs)  \
-\                 |] ==> R(x . CONS(z,zs))  \
+\       !!x.      [| x: A |] ==> R(x$NIL);  \
+\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x$zs)  \
+\                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
 by (rtac (major RS Term_induct) 1);
 by (etac List_induct 1);
@@ -97,7 +97,7 @@
 (*Induction for the abstract type 'a term*)
 val prems = goal Term.thy 
     "[| !!x. R(App(x,Nil));  \
-\       !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts)))  \
+\       !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts))  \
 \    |] ==> R(t)";
 by (rtac term_induct 1);  (*types force good instantiation*)
 by (etac rev_mp 1);
@@ -117,7 +117,7 @@
 val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
 
 (*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M.N : Term(A)";
+val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M$N : Term(A)";
 by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
 val APP_I = result();
 
@@ -143,7 +143,7 @@
 
 val [prem1,prem2,A_subset_Sexp] = goal Term.thy
     "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
-\    Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
+\    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (rtac (Split RS trans) 1);
 by (simp_tac (HOL_ss addsimps
diff -r 69d815b0e1eb -r 21291189b51e ex/Term.thy
--- a/ex/Term.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Term.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -32,7 +32,7 @@
   Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
   Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
     (*defining the abstract constants*)
-  App_def 	"App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
+  App_def 	"App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
      (*list recursion*)
   Term_rec_def	
    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
diff -r 69d815b0e1eb -r 21291189b51e ex/insort.thy
--- a/ex/insort.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/insort.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -14,9 +14,9 @@
 
 rules
   ins_Nil  "ins(f,x,[]) = [x]"
-  ins_Cons "ins(f,x,Cons(y,ys)) =   \
-\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+  ins_Cons "ins(f,x,y#ys) =   \
+\	       if(f(x,y), x#y#ys, y# ins(f,x,ys))"
 
   insort_Nil  "insort(f,[]) = []"
-  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+  insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
 end
diff -r 69d815b0e1eb -r 21291189b51e ex/pl.ML
--- a/ex/pl.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/pl.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -158,7 +158,7 @@
 by (simp_tac pl_ss 1);
 val hyps_false = result();
 
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
+goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, (#v)->false)}";
 by (simp_tac pl_ss 1);
 val hyps_var = result();
 
@@ -250,7 +250,7 @@
 
 (*For the case hyps(p,t)-insert(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-goal PL.thy "!p.hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})";
+goal PL.thy "!p.hyps(p, t-{v}) <= insert((#v)->false, hyps(p,t)-{#v})";
 by (rtac pl_ind 1);
 by (simp_tac pl_ss 1);
 by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -260,8 +260,8 @@
 val hyps_Diff = result() RS spec;
 
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
-  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
-goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})";
+  we also have hyps(p,t)-{(#v)->false} <= hyps(p, insert(v,t)) *)
+goal PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
 by (rtac pl_ind 1);
 by (simp_tac pl_ss 1);
 by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
@@ -282,7 +282,7 @@
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
-goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
+goal PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, (#v)->false})";
 by (rtac pl_ind 1);
 by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
               fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
diff -r 69d815b0e1eb -r 21291189b51e ex/pl.thy
--- a/ex/pl.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/pl.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -46,7 +46,7 @@
 eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
 
 hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
 
 var_inject "(#v = #w) ==> v = w"
 imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R"
diff -r 69d815b0e1eb -r 21291189b51e ex/qsort.thy
--- a/ex/qsort.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/qsort.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -13,8 +13,8 @@
 rules
 
 qsort_Nil  "qsort(le,[]) = []"
-qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
-\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
+qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ \
+\                            (x# qsort(le,[y:xs . le(x,y)]))"
 
 (* computational induction.
    The dependence of p on x but not xs is intentional.
@@ -22,6 +22,6 @@
 qsort_ind
  "[| P([]); \
 \    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
-\            P(Cons(x,xs)) |] \
+\            P(x#xs) |] \
 \ ==> P(xs)"
 end
diff -r 69d815b0e1eb -r 21291189b51e ex/simult.thy
--- a/ex/simult.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/simult.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -50,7 +50,7 @@
 	"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
 
      (*the concrete constants*)
-  TCONS_def 	"TCONS(M,N) == In0(M . N)"
+  TCONS_def 	"TCONS(M,N) == In0(M $ N)"
   FNIL_def	"FNIL       == In1(NIL)"
   FCONS_def	"FCONS(M,N) == In1(CONS(M,N))"
      (*the abstract constants*)
diff -r 69d815b0e1eb -r 21291189b51e ex/sorting.thy
--- a/ex/sorting.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/sorting.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -18,13 +18,13 @@
 
 sorted1_Nil  "sorted1(f,[])"
 sorted1_One  "sorted1(f,[x])"
-sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
 
 sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
 
 mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
 
 total_def  "total(r) == (!x y. r(x,y) | r(y,x))"
 transf_def "transf(f) == (!x y z. f(x,y) & f(y,z) --> f(x,z))"
diff -r 69d815b0e1eb -r 21291189b51e ex/term.ML
--- a/ex/term.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/term.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -40,7 +40,7 @@
 val [major,minor] = goal Term.thy 
     "[| M: Term(A);  \
 \       !!x zs. [| x: A;  zs: List(Term(A));  zs: List({x.R(x)}) \
-\               |] ==> R(x.zs)  \
+\               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS (Term_def RS def_induct)) 1);
 by (rtac Term_fun_mono 1);
@@ -51,9 +51,9 @@
 (*Induction on Term(A) followed by induction on List *)
 val major::prems = goal Term.thy
     "[| M: Term(A);  \
-\       !!x.      [| x: A |] ==> R(x.NIL);  \
-\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x.zs)  \
-\                 |] ==> R(x . CONS(z,zs))  \
+\       !!x.      [| x: A |] ==> R(x$NIL);  \
+\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x$zs)  \
+\                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
 by (rtac (major RS Term_induct) 1);
 by (etac List_induct 1);
@@ -97,7 +97,7 @@
 (*Induction for the abstract type 'a term*)
 val prems = goal Term.thy 
     "[| !!x. R(App(x,Nil));  \
-\       !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts)))  \
+\       !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts))  \
 \    |] ==> R(t)";
 by (rtac term_induct 1);  (*types force good instantiation*)
 by (etac rev_mp 1);
@@ -117,7 +117,7 @@
 val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
 
 (*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M.N : Term(A)";
+val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M$N : Term(A)";
 by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
 val APP_I = result();
 
@@ -143,7 +143,7 @@
 
 val [prem1,prem2,A_subset_Sexp] = goal Term.thy
     "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
-\    Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
+\    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (rtac (Split RS trans) 1);
 by (simp_tac (HOL_ss addsimps
diff -r 69d815b0e1eb -r 21291189b51e ex/term.thy
--- a/ex/term.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/term.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -32,7 +32,7 @@
   Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
   Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
     (*defining the abstract constants*)
-  App_def 	"App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
+  App_def 	"App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
      (*list recursion*)
   Term_rec_def	
    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
diff -r 69d815b0e1eb -r 21291189b51e hol.ML
--- a/hol.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/hol.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -337,6 +337,7 @@
 fun sstac ths = EVERY' (map stac ths);
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
+
 end;
 
 open HOL_Lemmas;
diff -r 69d815b0e1eb -r 21291189b51e sexp.ML
--- a/sexp.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/sexp.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -20,7 +20,7 @@
 
 val major::prems = goal Sexp.thy 
     "[| ii: Sexp;  !!a. P(Leaf(a));   !!k. P(Numb(k));   \
-\       !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i.j) \
+\       !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \
 \    |]  ==> P(ii)";
 by (rtac (major RS (Sexp_def RS def_induct)) 1);
 by (rtac Sexp_fun_mono 1);
@@ -41,7 +41,7 @@
 		     addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
 val Sexp_case_Numb = result();
 
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M.N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
 by (fast_tac (HOL_cs addIs  [select_equality] 
 	             addSDs [Scons_inject]
 	             addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
@@ -61,7 +61,7 @@
 val Sexp_NumbI = result();
 
 val prems = goal Sexp.thy 
-    "[| M: Sexp;  N: Sexp |] ==> M.N : Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> M$N : Sexp";
 by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
 val Sexp_SconsI = result();
 
@@ -79,7 +79,7 @@
 by (fast_tac (set_cs addIs [SexpI]) 1);
 val range_Leaf_subset_Sexp = result();
 
-val [major] = goal Sexp.thy "M.N : Sexp ==> M: Sexp & N: Sexp";
+val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac Sexp_induct 1);
 by (ALLGOALS 
@@ -101,12 +101,12 @@
     pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
 
 val prems = goalw Sexp.thy [pred_Sexp_def]
-    "[| M: Sexp;  N: Sexp |] ==> <M, M.N> : pred_Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> <M, M$N> : pred_Sexp";
 by (fast_tac (set_cs addIs prems) 1);
 val pred_SexpI1 = result();
 
 val prems = goalw Sexp.thy [pred_Sexp_def]
-    "[| M: Sexp;  N: Sexp |] ==> <N, M.N> : pred_Sexp";
+    "[| M: Sexp;  N: Sexp |] ==> <N, M$N> : pred_Sexp";
 by (fast_tac (set_cs addIs prems) 1);
 val pred_SexpI2 = result();
 
@@ -126,8 +126,8 @@
 
 val major::prems = goalw Sexp.thy [pred_Sexp_def]
     "[| p : pred_Sexp;  \
-\       !!M N. [| p = <M, M.N>;  M: Sexp;  N: Sexp |] ==> R; \
-\       !!M N. [| p = <N, M.N>;  M: Sexp;  N: Sexp |] ==> R  \
+\       !!M N. [| p = <M, M$N>;  M: Sexp;  N: Sexp |] ==> R; \
+\       !!M N. [| p = <N, M$N>;  M: Sexp;  N: Sexp |] ==> R  \
 \    |] ==> R";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
@@ -159,7 +159,7 @@
 val Sexp_rec_Numb = result();
 
 goal Sexp.thy "!!M. [| M: Sexp;  N: Sexp |] ==> \
-\    Sexp_rec(M.N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
+\    Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
 by (rtac (Sexp_rec_unfold RS trans) 1);
 by (asm_simp_tac(HOL_ss addsimps
                [Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
diff -r 69d815b0e1eb -r 21291189b51e sexp.thy
--- a/sexp.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/sexp.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -24,10 +24,10 @@
   Sexp_case_def	
    "Sexp_case(M,c,d,e) == @ z. (? x.   M=Leaf(x) & z=c(x))  \
 \                            | (? k.   M=Numb(k) & z=d(k))  \
-\                            | (? N1 N2. M = N1 . N2  & z=e(N1,N2))"
+\                            | (? N1 N2. M = N1 $ N2  & z=e(N1,N2))"
 
   pred_Sexp_def
-     "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M.N>, <N, M.N>}"
+     "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}"
 
   Sexp_rec_def
    "Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M,  \
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));
diff -r 69d815b0e1eb -r 21291189b51e univ.thy
--- a/univ.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/univ.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -29,7 +29,7 @@
   Atom      :: "('a+nat) => 'a node set"
   Leaf      :: "'a => 'a node set"
   Numb      :: "nat => 'a node set"
-  "."       :: "['a node set, 'a node set]=> 'a node set" 	(infixr 60)
+  "$"       :: "['a node set, 'a node set]=> 'a node set" 	(infixr 60)
   In0,In1   :: "'a node set => 'a node set"
 
   ntrunc    :: "[nat, 'a node set] => 'a node set"
@@ -67,26 +67,26 @@
 
   (*S-expression constructors*)
   Atom_def   "Atom == (%x. {Abs_Node(<%k.0, x>)})"
-  Scons_def  "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+  Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
 
   (*Leaf nodes, with arbitrary or nat labels*)
   Leaf_def   "Leaf == Atom o Inl"
   Numb_def   "Numb == Atom o Inr"
 
   (*Injections of the "disjoint sum"*)
-  In0_def    "In0(M) == Numb(0) . M"
-  In1_def    "In1(M) == Numb(Suc(0)) . M"
+  In0_def    "In0(M) == Numb(0) $ M"
+  In1_def    "In1(M) == Numb(Suc(0)) $ M"
 
   (*the set of nodes with depth less than k*)
   ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
   ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
-  uprod_def  "A<*>B == UN x:A. UN y:B. { (x.y) }"
+  uprod_def  "A<*>B == UN x:A. UN y:B. { (x$y) }"
   usum_def   "A<+>B == In0``A Un In1``B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)"
+  Split_def  "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
 
   Case_def   "Case(M,c,d) == @u.  (? x . M = In0(x) & u = c(x))	\
 \	   	                | (? y . M = In1(y) & u = d(y))"
@@ -97,7 +97,7 @@
   diag_def   "diag(A) == UN x:A. {<x,x>}"
 
   dprod_def  "r<**>s == UN u:r. UN v:s. \
-\                       split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))"
+\                       split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
 
   dsum_def   "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
 \                       (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"