Subst/AList.ML

 For AList.thy.
 *)
 
 open AList;
 
-(*********)
-
-val al_defs = [alist_rec_def,assoc_def];
-
-val alist_ss = prod_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq,
-                                list_rec_Nil,list_rec_Cons];
-
 val al_rews = 
-  let fun mk_thm s = prove_goalw AList.thy al_defs s 
-                            (fn _ => [simp_tac alist_ss 1])
+  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(Nil,c,d) = c",
+     ["alist_rec([],c,d) = c",
       "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
-      "assoc(v,d,Nil) = 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(Nil);   \
+    "[| P([]);   \
 \       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
-by (list_ind_tac "l" 1);
+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);

 
 (*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)];
-
-(*
-val prems = goal AList.thy
-    "[| 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));
-qed "alist_induct2";
-
-add_inds alist_induct2;
-*)