changed "." to "$" to eliminate ambiguity
authorclasohm
Tue Mar 22 12:42:56 1994 +0100 (1994-03-22)
changeset 28978541329ff35
parent 288 b00ce6a1fe27
child 290 37d580c16af5
changed "." to "$" to eliminate ambiguity
src/CCL/Hered.ML
src/CCL/Term.ML
src/CCL/Term.thy
src/CCL/Type.ML
src/CCL/Wfd.ML
src/CCL/Wfd.thy
src/CCL/coinduction.ML
src/CCL/eval.ML
src/CCL/hered.ML
src/CCL/term.ML
src/CCL/term.thy
src/CCL/type.ML
src/CCL/typecheck.ML
src/CCL/wfd.ML
src/CCL/wfd.thy
     1.1 --- a/src/CCL/Hered.ML	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/Hered.ML	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4                             "zero : HTT",
     1.5                             "succ(n) : HTT <-> n : HTT",
     1.6                             "[] : HTT",
     1.7 -                           "x.xs : HTT <-> x : HTT & xs : HTT"];
     1.8 +                           "x$xs : HTT <-> x : HTT & xs : HTT"];
     1.9  end;
    1.10  
    1.11  val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
    1.12 @@ -108,7 +108,7 @@
    1.13  \                         succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    1.14          "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    1.15          "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
    1.16 -\                         h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
    1.17 +\                         h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
    1.18  
    1.19  (*** Formation Rules for Types ***)
    1.20  
     2.1 --- a/src/CCL/Term.ML	Tue Mar 22 08:24:14 1994 +0100
     2.2 +++ b/src/CCL/Term.ML	Tue Mar 22 12:42:56 1994 +0100
     2.3 @@ -90,10 +90,10 @@
     2.4  val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
     2.5  
     2.6  val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
     2.7 -val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
     2.8 +val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
     2.9  val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
    2.10  val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
    2.11 -val lrecBcons  = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
    2.12 +val lrecBcons  = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
    2.13  val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
    2.14  
    2.15  val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
    2.16 @@ -120,12 +120,12 @@
    2.17                 ["(inl(a) = inl(a')) <-> (a=a')",
    2.18                  "(inr(a) = inr(a')) <-> (a=a')",
    2.19                  "(succ(a) = succ(a')) <-> (a=a')",
    2.20 -                "(a.b = a'.b') <-> (a=a' & b=b')"];
    2.21 +                "(a$b = a'$b') <-> (a=a' & b=b')"];
    2.22  
    2.23  (*** Constructors are distinct ***)
    2.24  
    2.25  val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
    2.26 -                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
    2.27 +                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
    2.28  
    2.29  (*** Rules for pre-order [= ***)
    2.30  
    2.31 @@ -136,7 +136,7 @@
    2.32    val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
    2.33                                  "inr(b) [= inr(b') <-> b [= b'",
    2.34                                  "succ(n) [= succ(n') <-> n [= n'",
    2.35 -                                "x.xs [= x'.xs' <-> x [= x'  & xs [= xs'"];
    2.36 +                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"];
    2.37  end;
    2.38  
    2.39  (*** Rewriting and Proving ***)
     3.1 --- a/src/CCL/Term.thy	Tue Mar 22 08:24:14 1994 +0100
     3.2 +++ b/src/CCL/Term.thy	Tue Mar 22 12:42:56 1994 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4    nrec       ::	      "[i,i,[i,i]=>i]=>i"
     3.5  
     3.6    nil        ::       "i"                    ("([])")
     3.7 -  "."        ::       "[i,i]=>i"             (infixr 80)
     3.8 +  "$"        ::       "[i,i]=>i"             (infixr 80)
     3.9    lcase      ::	      "[i,i,[i,i]=>i]=>i"
    3.10    lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
    3.11  
    3.12 @@ -60,7 +60,7 @@
    3.13    ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    3.14    nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    3.15    nil_def	              "[] == inl(one)"
    3.16 -  cons_def                   "h.t == inr(<h,t>)"
    3.17 +  cons_def                   "h$t == inr(<h,t>)"
    3.18    lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    3.19    lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    3.20  
     4.1 --- a/src/CCL/Type.ML	Tue Mar 22 08:24:14 1994 +0100
     4.2 +++ b/src/CCL/Type.ML	Tue Mar 22 12:42:56 1994 +0100
     4.3 @@ -183,9 +183,9 @@
     4.4  val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
     4.5  
     4.6  val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
     4.7 -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
     4.8 -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
     4.9 -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
    4.10 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
    4.11 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
    4.12 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
    4.13  
    4.14  val iXHs = [NatXH,ListXH];
    4.15  val icase_rls = XH_to_Es iXHs;
    4.16 @@ -198,7 +198,7 @@
    4.17  val zeroT = icanT_tac "zero : Nat";
    4.18  val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
    4.19  val nilT  = icanT_tac "[] : List(A)";
    4.20 -val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
    4.21 +val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h$t : List(A)";
    4.22  
    4.23  val icanTs = [zeroT,succT,nilT,consT];
    4.24  
    4.25 @@ -209,7 +209,7 @@
    4.26  
    4.27  val lcaseT = incanT_tac
    4.28       "[| l:List(A); l=[] ==> b:C([]); \
    4.29 -\        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
    4.30 +\        !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
    4.31  \     lcase(l,b,c) : C(l)";
    4.32  
    4.33  val incanTs = [ncaseT,lcaseT];
    4.34 @@ -230,7 +230,7 @@
    4.35  
    4.36  val List_ind = ind_tac
    4.37       "[| l:List(A); P([]); \
    4.38 -\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
    4.39 +\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
    4.40  \     P(l)";
    4.41  
    4.42  val inds = [Nat_ind,List_ind];
    4.43 @@ -250,7 +250,7 @@
    4.44  
    4.45  val lrecT = prec_tac
    4.46       "[| l:List(A); b:C([]); \
    4.47 -\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
    4.48 +\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>  \
    4.49  \     lrec(l,b,c) : C(l)";
    4.50  
    4.51  val precTs = [nrecT,lrecT];
    4.52 @@ -300,7 +300,7 @@
    4.53  (* EG *)
    4.54  
    4.55  val prems = goal Type.thy 
    4.56 -    "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
    4.57 +    "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
    4.58  by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
    4.59  br (letrecB RS ssubst) 1;
    4.60  bw cons_def;
     5.1 --- a/src/CCL/Wfd.ML	Tue Mar 22 08:24:14 1994 +0100
     5.2 +++ b/src/CCL/Wfd.ML	Tue Mar 22 12:42:56 1994 +0100
     5.3 @@ -179,7 +179,7 @@
     5.4  by (fast_tac set_cs 1);
     5.5  val NatPRXH = result();
     5.6  
     5.7 -goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
     5.8 +goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
     5.9  by (fast_tac set_cs 1);
    5.10  val ListPRXH = result();
    5.11  
     6.1 --- a/src/CCL/Wfd.thy	Tue Mar 22 08:24:14 1994 +0100
     6.2 +++ b/src/CCL/Wfd.thy	Tue Mar 22 12:42:56 1994 +0100
     6.3 @@ -30,5 +30,5 @@
     6.4    "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
     6.5  
     6.6    NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
     6.7 -  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
     6.8 +  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
     6.9  end
     7.1 --- a/src/CCL/coinduction.ML	Tue Mar 22 08:24:14 1994 +0100
     7.2 +++ b/src/CCL/coinduction.ML	Tue Mar 22 12:42:56 1994 +0100
     7.3 @@ -60,7 +60,7 @@
     7.4         "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
     7.5         "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); \
     7.6  \          <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> \
     7.7 -\       <h.t,h'.t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
     7.8 +\       <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
     7.9  
    7.10  fun POgen_tac (rla,rlb) i =
    7.11         SELECT_GOAL (safe_tac ccl_cs) i THEN
    7.12 @@ -90,7 +90,7 @@
    7.13   "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    7.14   "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
    7.15  \          <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \
    7.16 -\       <h.t,h'.t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
    7.17 +\       <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
    7.18  
    7.19  fun EQgen_raw_tac i =
    7.20         (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ 
     8.1 --- a/src/CCL/eval.ML	Tue Mar 22 08:24:14 1994 +0100
     8.2 +++ b/src/CCL/eval.ML	Tue Mar 22 12:42:56 1994 +0100
     8.3 @@ -58,11 +58,11 @@
     8.4                "[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c",
     8.5                "[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c",
     8.6                "[] ---> []",
     8.7 -              "h.t ---> h.t",
     8.8 +              "h$t ---> h$t",
     8.9                "[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c",
    8.10 -              "[| l ---> x.xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
    8.11 +              "[| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
    8.12                "[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c",
    8.13 -              "[| l--->x.xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
    8.14 +              "[| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
    8.15  
    8.16  EVal_rls := !EVal_rls @ V_rls;
    8.17  
    8.18 @@ -93,12 +93,12 @@
    8.19  (* Reverse *)
    8.20  
    8.21  val prems = goal thy
    8.22 -    "letrec id l be lcase(l,[],%x xs.x.id(xs)) \
    8.23 -\              in id(zero.succ(zero).[]) ---> ?a";
    8.24 +    "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
    8.25 +\              in id(zero$succ(zero)$[]) ---> ?a";
    8.26  by (ceval_tac []);
    8.27  
    8.28  val prems = goal thy
    8.29 -    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x.[],%y ys g.y.g)) \
    8.30 -\              in rev(zero.succ(zero).(succ((lam x.x)`succ(zero))).([])) ---> ?a";
    8.31 +    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
    8.32 +\              in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
    8.33  by (ceval_tac []);
    8.34  
     9.1 --- a/src/CCL/hered.ML	Tue Mar 22 08:24:14 1994 +0100
     9.2 +++ b/src/CCL/hered.ML	Tue Mar 22 12:42:56 1994 +0100
     9.3 @@ -70,7 +70,7 @@
     9.4                             "zero : HTT",
     9.5                             "succ(n) : HTT <-> n : HTT",
     9.6                             "[] : HTT",
     9.7 -                           "x.xs : HTT <-> x : HTT & xs : HTT"];
     9.8 +                           "x$xs : HTT <-> x : HTT & xs : HTT"];
     9.9  end;
    9.10  
    9.11  val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
    9.12 @@ -108,7 +108,7 @@
    9.13  \                         succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    9.14          "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    9.15          "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
    9.16 -\                         h.t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
    9.17 +\                         h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
    9.18  
    9.19  (*** Formation Rules for Types ***)
    9.20  
    10.1 --- a/src/CCL/term.ML	Tue Mar 22 08:24:14 1994 +0100
    10.2 +++ b/src/CCL/term.ML	Tue Mar 22 12:42:56 1994 +0100
    10.3 @@ -90,10 +90,10 @@
    10.4  val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
    10.5  
    10.6  val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
    10.7 -val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
    10.8 +val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
    10.9  val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
   10.10  val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
   10.11 -val lrecBcons  = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
   10.12 +val lrecBcons  = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
   10.13  val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
   10.14  
   10.15  val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
   10.16 @@ -120,12 +120,12 @@
   10.17                 ["(inl(a) = inl(a')) <-> (a=a')",
   10.18                  "(inr(a) = inr(a')) <-> (a=a')",
   10.19                  "(succ(a) = succ(a')) <-> (a=a')",
   10.20 -                "(a.b = a'.b') <-> (a=a' & b=b')"];
   10.21 +                "(a$b = a'$b') <-> (a=a' & b=b')"];
   10.22  
   10.23  (*** Constructors are distinct ***)
   10.24  
   10.25  val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
   10.26 -                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
   10.27 +                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
   10.28  
   10.29  (*** Rules for pre-order [= ***)
   10.30  
   10.31 @@ -136,7 +136,7 @@
   10.32    val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
   10.33                                  "inr(b) [= inr(b') <-> b [= b'",
   10.34                                  "succ(n) [= succ(n') <-> n [= n'",
   10.35 -                                "x.xs [= x'.xs' <-> x [= x'  & xs [= xs'"];
   10.36 +                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"];
   10.37  end;
   10.38  
   10.39  (*** Rewriting and Proving ***)
    11.1 --- a/src/CCL/term.thy	Tue Mar 22 08:24:14 1994 +0100
    11.2 +++ b/src/CCL/term.thy	Tue Mar 22 12:42:56 1994 +0100
    11.3 @@ -28,7 +28,7 @@
    11.4    nrec       ::	      "[i,i,[i,i]=>i]=>i"
    11.5  
    11.6    nil        ::       "i"                    ("([])")
    11.7 -  "."        ::       "[i,i]=>i"             (infixr 80)
    11.8 +  "$"        ::       "[i,i]=>i"             (infixr 80)
    11.9    lcase      ::	      "[i,i,[i,i]=>i]=>i"
   11.10    lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
   11.11  
   11.12 @@ -60,7 +60,7 @@
   11.13    ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
   11.14    nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
   11.15    nil_def	              "[] == inl(one)"
   11.16 -  cons_def                   "h.t == inr(<h,t>)"
   11.17 +  cons_def                   "h$t == inr(<h,t>)"
   11.18    lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
   11.19    lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
   11.20  
    12.1 --- a/src/CCL/type.ML	Tue Mar 22 08:24:14 1994 +0100
    12.2 +++ b/src/CCL/type.ML	Tue Mar 22 12:42:56 1994 +0100
    12.3 @@ -183,9 +183,9 @@
    12.4  val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
    12.5  
    12.6  val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
    12.7 -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
    12.8 -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
    12.9 -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
   12.10 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
   12.11 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
   12.12 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
   12.13  
   12.14  val iXHs = [NatXH,ListXH];
   12.15  val icase_rls = XH_to_Es iXHs;
   12.16 @@ -198,7 +198,7 @@
   12.17  val zeroT = icanT_tac "zero : Nat";
   12.18  val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
   12.19  val nilT  = icanT_tac "[] : List(A)";
   12.20 -val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
   12.21 +val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h$t : List(A)";
   12.22  
   12.23  val icanTs = [zeroT,succT,nilT,consT];
   12.24  
   12.25 @@ -209,7 +209,7 @@
   12.26  
   12.27  val lcaseT = incanT_tac
   12.28       "[| l:List(A); l=[] ==> b:C([]); \
   12.29 -\        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
   12.30 +\        !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
   12.31  \     lcase(l,b,c) : C(l)";
   12.32  
   12.33  val incanTs = [ncaseT,lcaseT];
   12.34 @@ -230,7 +230,7 @@
   12.35  
   12.36  val List_ind = ind_tac
   12.37       "[| l:List(A); P([]); \
   12.38 -\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
   12.39 +\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
   12.40  \     P(l)";
   12.41  
   12.42  val inds = [Nat_ind,List_ind];
   12.43 @@ -250,7 +250,7 @@
   12.44  
   12.45  val lrecT = prec_tac
   12.46       "[| l:List(A); b:C([]); \
   12.47 -\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
   12.48 +\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>  \
   12.49  \     lrec(l,b,c) : C(l)";
   12.50  
   12.51  val precTs = [nrecT,lrecT];
   12.52 @@ -300,7 +300,7 @@
   12.53  (* EG *)
   12.54  
   12.55  val prems = goal Type.thy 
   12.56 -    "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
   12.57 +    "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
   12.58  by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
   12.59  br (letrecB RS ssubst) 1;
   12.60  bw cons_def;
    13.1 --- a/src/CCL/typecheck.ML	Tue Mar 22 08:24:14 1994 +0100
    13.2 +++ b/src/CCL/typecheck.ML	Tue Mar 22 12:42:56 1994 +0100
    13.3 @@ -25,7 +25,7 @@
    13.4              "P(zero) ==> zero : {x:Nat.P(x)}",
    13.5              "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
    13.6              "P([]) ==> [] : {x:List(A).P(x)}",
    13.7 -            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
    13.8 +            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
    13.9          ] end;
   13.10  *)
   13.11  val Subtype_canTs = 
   13.12 @@ -38,7 +38,7 @@
   13.13              "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
   13.14              "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
   13.15              "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
   13.16 -            "h : {x:A. t : {y:List(A).P(x.y)}} ==> h.t : {x:List(A).P(x)}"
   13.17 +            "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
   13.18          ] end;
   13.19  
   13.20  val prems = goal Type.thy
    14.1 --- a/src/CCL/wfd.ML	Tue Mar 22 08:24:14 1994 +0100
    14.2 +++ b/src/CCL/wfd.ML	Tue Mar 22 12:42:56 1994 +0100
    14.3 @@ -179,7 +179,7 @@
    14.4  by (fast_tac set_cs 1);
    14.5  val NatPRXH = result();
    14.6  
    14.7 -goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
    14.8 +goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
    14.9  by (fast_tac set_cs 1);
   14.10  val ListPRXH = result();
   14.11  
    15.1 --- a/src/CCL/wfd.thy	Tue Mar 22 08:24:14 1994 +0100
    15.2 +++ b/src/CCL/wfd.thy	Tue Mar 22 12:42:56 1994 +0100
    15.3 @@ -30,5 +30,5 @@
    15.4    "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
    15.5  
    15.6    NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
    15.7 -  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
    15.8 +  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
    15.9  end