src/HOL/Sexp.ML
changeset 1475 7f5a4cd08209
parent 1465 5d7a7e439cec
child 1642 21db0cf9a1a4
--- 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)";