--- a/Subst/AList.ML Fri Nov 11 10:35:03 1994 +0100
+++ b/Subst/AList.ML Mon Nov 21 17:50:34 1994 +0100
@@ -34,7 +34,7 @@
by (etac ssubst 1);
by (resolve_tac prems 1);
by (assume_tac 1);
-val alist_induct = result();
+qed "alist_induct";
(*Perform induction on xs. *)
fun alist_ind_tac a M =
@@ -46,7 +46,7 @@
"[| P(Nil); !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
by (alist_ind_tac "a" 1);
by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
-val alist_induct2 = result();
+qed "alist_induct2";
add_inds alist_induct2;
*)