src/HOL/Sexp.ML
changeset 5191 8ceaa19f7717
parent 5143 b94cd208f073
child 5278 a903b66822e2
     1.1 --- a/src/HOL/Sexp.ML	Fri Jul 24 13:36:49 1998 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Fri Jul 24 13:39:47 1998 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "sexp_case_Numb";
     1.6  
     1.7 -Goalw [sexp_case_def] "sexp_case c d e (M$N) = e M N";
     1.8 +Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
     1.9  by (Blast_tac 1);
    1.10  qed "sexp_case_Scons";
    1.11  
    1.12 @@ -41,7 +41,7 @@
    1.13  by (Blast_tac 1);
    1.14  qed "range_Leaf_subset_sexp";
    1.15  
    1.16 -val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    1.17 +val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
    1.18  by (rtac (major RS setup_induction) 1);
    1.19  by (etac sexp.induct 1);
    1.20  by (ALLGOALS Blast_tac);
    1.21 @@ -60,12 +60,12 @@
    1.22      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    1.23  
    1.24  Goalw [pred_sexp_def]
    1.25 -    "!!M. [| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    1.26 +    "!!M. [| M: sexp;  N: sexp |] ==> (M, Scons M N) : pred_sexp";
    1.27  by (Blast_tac 1);
    1.28  qed "pred_sexpI1";
    1.29  
    1.30  Goalw [pred_sexp_def]
    1.31 -    "!!M. [| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    1.32 +    "!!M. [| M: sexp;  N: sexp |] ==> (N, Scons M N) : pred_sexp";
    1.33  by (Blast_tac 1);
    1.34  qed "pred_sexpI2";
    1.35  
    1.36 @@ -82,8 +82,8 @@
    1.37  
    1.38  val major::prems = goalw Sexp.thy [pred_sexp_def]
    1.39      "[| p : pred_sexp;                                       \
    1.40 -\       !!M N. [| p = (M, M$N);  M: sexp;  N: sexp |] ==> R; \
    1.41 -\       !!M N. [| p = (N, M$N);  M: sexp;  N: sexp |] ==> R  \
    1.42 +\       !!M N. [| p = (M, Scons M N);  M: sexp;  N: sexp |] ==> R; \
    1.43 +\       !!M N. [| p = (N, Scons M N);  M: sexp;  N: sexp |] ==> R  \
    1.44  \    |] ==> R";
    1.45  by (cut_facts_tac [major] 1);
    1.46  by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
    1.47 @@ -125,7 +125,7 @@
    1.48  qed "sexp_rec_Numb";
    1.49  
    1.50  Goal "[| M: sexp;  N: sexp |] ==> \
    1.51 -\    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
    1.52 +\    sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
    1.53  by (rtac (sexp_rec_unfold RS trans) 1);
    1.54  by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
    1.55  qed "sexp_rec_Scons";