alist_rec and assoc are now defined using primrec and thus no longer
refer to the recursion combinator list_rec, which should be considered
internal.
(* Title: Subst/AList.ML
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Association lists.
*)
open AList;
val prems = goal AList.thy
"[| P([]); \
\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)";
by (induct_tac "l" 1);
by (split_all_tac 2);
by (REPEAT (ares_tac prems 1));
qed "alist_induct";
(*Perform induction on xs. *)
fun alist_ind_tac a M =
EVERY [res_inst_tac [("l",a)] alist_induct M,
rename_last_tac a ["1"] (M+1)];