--- a/src/HOL/Sexp.ML Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Sexp.ML Thu Sep 12 10:40:05 1996 +0200
@@ -10,17 +10,6 @@
(** sexp_case **)
-val sexp_free_cs =
- set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject]
- addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
- Numb_neq_Scons, Numb_neq_Leaf,
- Scons_neq_Leaf, Scons_neq_Numb];
-
-AddSDs [Leaf_inject, Numb_inject, Scons_inject];
-AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
- Numb_neq_Scons, Numb_neq_Leaf,
- Scons_neq_Leaf, Scons_neq_Numb];
-
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
by (resolve_tac [select_equality] 1);
by (ALLGOALS (Fast_tac));
@@ -60,8 +49,7 @@
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
- (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
+by (ALLGOALS Fast_tac);
qed "Scons_D";
(** Introduction rules for 'pred_sexp' **)
@@ -109,9 +97,7 @@
goal Sexp.thy "wf(pred_sexp)";
by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
by (etac sexp.induct 1);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
+by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
qed "wf_pred_sexp";
(*** sexp_rec -- by wf recursion on pred_sexp ***)