--- a/src/HOL/Sexp.ML Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Sexp.ML Mon Feb 05 21:27:16 1996 +0100
@@ -17,17 +17,17 @@
Scons_neq_Leaf, Scons_neq_Numb];
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Leaf";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Numb";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
-by (rtac select_equality 1);
+by (resolve_tac [select_equality] 1);
by (ALLGOALS (fast_tac sexp_free_cs));
qed "sexp_case_Scons";
@@ -109,9 +109,18 @@
(*** sexp_rec -- by wf recursion on pred_sexp ***)
+goal Sexp.thy
+ "(%M. sexp_rec M c d e) = wfrec pred_sexp \
+ \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
+by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+bind_thm("sexp_rec_unfold", wf_pred_sexp RS
+ ((result() RS eq_reflection) RS def_wfrec));
(** conversion rules **)
-val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
+(*---------------------------------------------------------------------------
+ * Old:
+ * val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";