--- a/Subst/AList.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Substitutions/AList.ML
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-For AList.thy.
-*)
-
-open AList;
-
-val al_rews =
- let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s
- (fn _ => [simp_tac list_ss 1])
- in map mk_thm
- ["alist_rec([],c,d) = c",
- "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
- "assoc(v,d,[]) = d",
- "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
-
-val prems = goal AList.thy
- "[| P([]); \
-\ !!x y xs. P(xs) ==> P(<x,y>#xs) |] ==> P(l)";
-by (list.induct_tac "l" 1);
-by (resolve_tac prems 1);
-by (rtac PairE 1);
-by (etac ssubst 1);
-by (resolve_tac prems 1);
-by (assume_tac 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)];