diff -r 3a8d722fd3ff -r 16c4ea954511 Subst/AList.ML --- 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(#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; *)