# HG changeset patch
# User clasohm
# Date 764336631 -3600
# Node ID 37d580c16af520a77872dadb0acfbe1a60eebc22
# Parent  78541329ff35a03f20ac3588bdb1fa2a0ac119c9
changed "." to "$" and added parentheses to eliminate ambiguity

diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Flag.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -29,9 +29,9 @@
   flag_def    "flag == lam l.letrec \
 \      flagx l be lcase(l,<[],<[],[]>>, \
 \                       %h t. split(flagx(t),%lr p.split(p,%lw lb. \
-\                            ccase(h, <red.lr,<lw,lb>>, \
-\                                     <lr,<white.lw,lb>>, \
-\                                     <lr,<lw,blue.lb>>)))) \
+\                            ccase(h, <red$lr,<lw,lb>>, \
+\                                     <lr,<white$lw,lb>>, \
+\                                     <lr,<lw,blue$lb>>)))) \
 \      in flagx(l)"    
 
   Flag_def
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/List.ML
--- a/src/CCL/ex/List.ML	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/List.ML	Tue Mar 22 12:43:51 1994 +0100
@@ -17,15 +17,15 @@
      ["(f o g) = (%a.f(g(a)))",
       "(f o g)(a) = f(g(a))",
       "map(f,[]) = []",
-      "map(f,x.xs) = f(x).map(f,xs)",
+      "map(f,x$xs) = f(x)$map(f,xs)",
       "[] @ m = m",
-      "x.xs @ m = x.(xs @ m)",
+      "x$xs @ m = x$(xs @ m)",
       "filter(f,[]) = []",
-      "filter(f,x.xs) = if f`x then x.filter(f,xs) else filter(f,xs)",
+      "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)",
       "flat([]) = []",
-      "flat(x.xs) = x @ flat(xs)",
-      "insert(f,a,[]) = a.[]",
-      "insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
+      "flat(x$xs) = x @ flat(xs)",
+      "insert(f,a,[]) = a$[]",
+      "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"];
 
 val list_ss = nat_ss addsimps listBs;
 
@@ -36,7 +36,7 @@
 by (ALLGOALS (asm_simp_tac list_ss));
 val nmapBnil = result();
 
-val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
+val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
 br (prem RS Nat_ind) 1;
 by (ALLGOALS (asm_simp_tac list_ss));
 val nmapBcons = result();
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/List.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -22,23 +22,23 @@
 
 rules 
 
-  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x).g)"
+  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x)$g)"
   comp_def    "f o g == (%x.f(g(x)))"
-  append_def  "l @ m == lrec(l,m,%x xs g.x.g)"
+  append_def  "l @ m == lrec(l,m,%x xs g.x$g)"
   mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
-  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
+  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
   flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
 
-  insert_def  "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
+  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
   isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
 
   partition_def 
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
-\                            if f`x then part(xs,x.a,b) else part(xs,a,x.b)) \
+\                            if f`x then part(xs,x$a,b) else part(xs,a,x$b)) \
 \                    in part(l,[],[])"
   qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
 \                                   let p be partition(f`h,t) \
-\                                   in split(p,%x y.qsortx(x) @ h.qsortx(y))) \
+\                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) \
 \                          in qsortx(l)"
 
 end
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/Stream.ML
--- a/src/CCL/ex/Stream.ML	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Stream.ML	Tue Mar 22 12:43:51 1994 +0100
@@ -82,21 +82,21 @@
 
 (*** The equivalance of two versions of an iteration function       ***)
 (*                                                                    *)
-(*        fun iter1(f,a) = a.iter1(f,f(a))                            *)
-(*        fun iter2(f,a) = a.map(f,iter2(f,a))                        *)
+(*        fun iter1(f,a) = a$iter1(f,f(a))                            *)
+(*        fun iter2(f,a) = a$map(f,iter2(f,a))                        *)
 
-goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
+goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
 br (letrecB RS trans) 1;
 by (simp_tac term_ss 1);
 val iter1B = result();
 
-goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
+goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
 br (letrecB RS trans) 1;
 br refl 1;
 val iter2B = result();
 
 val [prem] =goal Stream.thy
-   "n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
+   "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
 br (iter2B RS ssubst) 1;back();back();
 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
 val iter2Blemma = result();
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/Stream.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -14,7 +14,7 @@
 
 rules 
 
-  iter1_def   "iter1(f,a) == letrec iter x be x.iter(f(x)) in iter(a)"
-  iter2_def   "iter2(f,a) == letrec iter x be x.map(f,iter(x)) in iter(a)"
+  iter1_def   "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
+  iter2_def   "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
 
 end
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/flag.thy
--- a/src/CCL/ex/flag.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/flag.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -29,9 +29,9 @@
   flag_def    "flag == lam l.letrec \
 \      flagx l be lcase(l,<[],<[],[]>>, \
 \                       %h t. split(flagx(t),%lr p.split(p,%lw lb. \
-\                            ccase(h, <red.lr,<lw,lb>>, \
-\                                     <lr,<white.lw,lb>>, \
-\                                     <lr,<lw,blue.lb>>)))) \
+\                            ccase(h, <red$lr,<lw,lb>>, \
+\                                     <lr,<white$lw,lb>>, \
+\                                     <lr,<lw,blue$lb>>)))) \
 \      in flagx(l)"    
 
   Flag_def
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/list.ML
--- a/src/CCL/ex/list.ML	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/list.ML	Tue Mar 22 12:43:51 1994 +0100
@@ -17,15 +17,15 @@
      ["(f o g) = (%a.f(g(a)))",
       "(f o g)(a) = f(g(a))",
       "map(f,[]) = []",
-      "map(f,x.xs) = f(x).map(f,xs)",
+      "map(f,x$xs) = f(x)$map(f,xs)",
       "[] @ m = m",
-      "x.xs @ m = x.(xs @ m)",
+      "x$xs @ m = x$(xs @ m)",
       "filter(f,[]) = []",
-      "filter(f,x.xs) = if f`x then x.filter(f,xs) else filter(f,xs)",
+      "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)",
       "flat([]) = []",
-      "flat(x.xs) = x @ flat(xs)",
-      "insert(f,a,[]) = a.[]",
-      "insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
+      "flat(x$xs) = x @ flat(xs)",
+      "insert(f,a,[]) = a$[]",
+      "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"];
 
 val list_ss = nat_ss addsimps listBs;
 
@@ -36,7 +36,7 @@
 by (ALLGOALS (asm_simp_tac list_ss));
 val nmapBnil = result();
 
-val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
+val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
 br (prem RS Nat_ind) 1;
 by (ALLGOALS (asm_simp_tac list_ss));
 val nmapBcons = result();
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/list.thy
--- a/src/CCL/ex/list.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/list.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -22,23 +22,23 @@
 
 rules 
 
-  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x).g)"
+  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x)$g)"
   comp_def    "f o g == (%x.f(g(x)))"
-  append_def  "l @ m == lrec(l,m,%x xs g.x.g)"
+  append_def  "l @ m == lrec(l,m,%x xs g.x$g)"
   mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
-  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
+  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
   flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
 
-  insert_def  "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
+  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
   isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
 
   partition_def 
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
-\                            if f`x then part(xs,x.a,b) else part(xs,a,x.b)) \
+\                            if f`x then part(xs,x$a,b) else part(xs,a,x$b)) \
 \                    in part(l,[],[])"
   qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
 \                                   let p be partition(f`h,t) \
-\                                   in split(p,%x y.qsortx(x) @ h.qsortx(y))) \
+\                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) \
 \                          in qsortx(l)"
 
 end
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/stream.ML
--- a/src/CCL/ex/stream.ML	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/stream.ML	Tue Mar 22 12:43:51 1994 +0100
@@ -82,21 +82,21 @@
 
 (*** The equivalance of two versions of an iteration function       ***)
 (*                                                                    *)
-(*        fun iter1(f,a) = a.iter1(f,f(a))                            *)
-(*        fun iter2(f,a) = a.map(f,iter2(f,a))                        *)
+(*        fun iter1(f,a) = a$iter1(f,f(a))                            *)
+(*        fun iter2(f,a) = a$map(f,iter2(f,a))                        *)
 
-goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
+goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
 br (letrecB RS trans) 1;
 by (simp_tac term_ss 1);
 val iter1B = result();
 
-goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
+goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
 br (letrecB RS trans) 1;
 br refl 1;
 val iter2B = result();
 
 val [prem] =goal Stream.thy
-   "n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
+   "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
 br (iter2B RS ssubst) 1;back();back();
 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
 val iter2Blemma = result();
diff -r 78541329ff35 -r 37d580c16af5 src/CCL/ex/stream.thy
--- a/src/CCL/ex/stream.thy	Tue Mar 22 12:42:56 1994 +0100
+++ b/src/CCL/ex/stream.thy	Tue Mar 22 12:43:51 1994 +0100
@@ -14,7 +14,7 @@
 
 rules 
 
-  iter1_def   "iter1(f,a) == letrec iter x be x.iter(f(x)) in iter(a)"
-  iter2_def   "iter2(f,a) == letrec iter x be x.map(f,iter(x)) in iter(a)"
+  iter1_def   "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
+  iter2_def   "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
 
 end