--- 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