src/CCL/Type.ML
changeset 289 78541329ff35
parent 8 c3d2c6dcf3f0
child 642 0db578095e6a
     1.1 --- a/src/CCL/Type.ML	Tue Mar 22 08:24:14 1994 +0100
     1.2 +++ b/src/CCL/Type.ML	Tue Mar 22 12:42:56 1994 +0100
     1.3 @@ -183,9 +183,9 @@
     1.4  val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
     1.5  
     1.6  val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
     1.7 -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
     1.8 -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
     1.9 -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
    1.10 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
    1.11 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
    1.12 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
    1.13  
    1.14  val iXHs = [NatXH,ListXH];
    1.15  val icase_rls = XH_to_Es iXHs;
    1.16 @@ -198,7 +198,7 @@
    1.17  val zeroT = icanT_tac "zero : Nat";
    1.18  val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
    1.19  val nilT  = icanT_tac "[] : List(A)";
    1.20 -val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
    1.21 +val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h$t : List(A)";
    1.22  
    1.23  val icanTs = [zeroT,succT,nilT,consT];
    1.24  
    1.25 @@ -209,7 +209,7 @@
    1.26  
    1.27  val lcaseT = incanT_tac
    1.28       "[| l:List(A); l=[] ==> b:C([]); \
    1.29 -\        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
    1.30 +\        !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
    1.31  \     lcase(l,b,c) : C(l)";
    1.32  
    1.33  val incanTs = [ncaseT,lcaseT];
    1.34 @@ -230,7 +230,7 @@
    1.35  
    1.36  val List_ind = ind_tac
    1.37       "[| l:List(A); P([]); \
    1.38 -\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
    1.39 +\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
    1.40  \     P(l)";
    1.41  
    1.42  val inds = [Nat_ind,List_ind];
    1.43 @@ -250,7 +250,7 @@
    1.44  
    1.45  val lrecT = prec_tac
    1.46       "[| l:List(A); b:C([]); \
    1.47 -\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
    1.48 +\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>  \
    1.49  \     lrec(l,b,c) : C(l)";
    1.50  
    1.51  val precTs = [nrecT,lrecT];
    1.52 @@ -300,7 +300,7 @@
    1.53  (* EG *)
    1.54  
    1.55  val prems = goal Type.thy 
    1.56 -    "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
    1.57 +    "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
    1.58  by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
    1.59  br (letrecB RS ssubst) 1;
    1.60  bw cons_def;