src/HOL/Sexp.ML
changeset 1985 84cf16192e03
parent 1760 6f41a494f3b1
child 2031 03a843f0f447
     1.1 --- a/src/HOL/Sexp.ML	Thu Sep 12 10:36:51 1996 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -10,17 +10,6 @@
     1.4  
     1.5  (** sexp_case **)
     1.6  
     1.7 -val sexp_free_cs = 
     1.8 -    set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] 
     1.9 -           addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    1.10 -                   Numb_neq_Scons, Numb_neq_Leaf,
    1.11 -                   Scons_neq_Leaf, Scons_neq_Numb];
    1.12 -
    1.13 -AddSDs [Leaf_inject, Numb_inject, Scons_inject];
    1.14 -AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    1.15 -                   Numb_neq_Scons, Numb_neq_Leaf,
    1.16 -                   Scons_neq_Leaf, Scons_neq_Numb];
    1.17 -
    1.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    1.19  by (resolve_tac [select_equality] 1);
    1.20  by (ALLGOALS (Fast_tac));
    1.21 @@ -60,8 +49,7 @@
    1.22  val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    1.23  by (rtac (major RS setup_induction) 1);
    1.24  by (etac sexp.induct 1);
    1.25 -by (ALLGOALS 
    1.26 -    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    1.27 +by (ALLGOALS Fast_tac);
    1.28  qed "Scons_D";
    1.29  
    1.30  (** Introduction rules for 'pred_sexp' **)
    1.31 @@ -109,9 +97,7 @@
    1.32  goal Sexp.thy "wf(pred_sexp)";
    1.33  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    1.34  by (etac sexp.induct 1);
    1.35 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    1.36 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    1.37 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    1.38 +by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
    1.39  qed "wf_pred_sexp";
    1.40  
    1.41  (*** sexp_rec -- by wf recursion on pred_sexp ***)