Mercurial Mercurial > repos > Old_HOL / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sexp.ML
changeset 48 21291189b51e
parent 0 7949f97df77a 
--- 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);
Old_HOL