Now uses the generic induct_tac

--- a/src/HOL/Auth/Event.ML	Thu Sep 11 12:21:34 1997 +0200
+++ b/src/HOL/Auth/Event.ML	Thu Sep 11 12:22:31 1997 +0200
@@ -76,7 +76,7 @@
 qed "UN_parts_sees_Notes";
 
 goal thy "Says A B X : set evs --> X : sees Spy evs";
-by (list.induct_tac "evs" 1);
+by (induct_tac "evs" 1);
 by (Auto_tac ());
 qed_spec_mp "Says_imp_sees_Spy";
 
@@ -111,16 +111,16 @@
 
 (*These two facts about "used" are unused.*)
 goal thy "used [] <= used l";
-by (list.induct_tac "l" 1);
-by (event.induct_tac "a" 2);
+by (induct_tac "l" 1);
+by (induct_tac "a" 2);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Blast_tac);
 qed "used_nil_subset";
 
 goal thy "used l <= used (l@l')";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
-by (event.induct_tac "a" 1);
+by (induct_tac "a" 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Blast_tac);
 qed "used_subset_append";

--- a/src/HOL/Auth/Public.ML	Thu Sep 11 12:21:34 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Thu Sep 11 12:22:31 1997 +0200
@@ -38,7 +38,7 @@
     -- not in normal form! **)
 
 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
-by (agent.induct_tac "C" 1);
+by (induct_tac "C" 1);
 by (auto_tac (!claset addIs [range_eqI], !simpset));
 qed "keysFor_parts_initState";
 Addsimps [keysFor_parts_initState];
@@ -48,22 +48,22 @@
 
 (*Agents see their own private keys!*)
 goal thy "A ~= Spy --> Key (priK A) : sees A evs";
-by (list.induct_tac "evs" 1);
-by (agent.induct_tac "A" 1);
+by (induct_tac "evs" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 qed_spec_mp "sees_own_priK";
 
 (*All public keys are visible to all*)
 goal thy "Key (pubK A) : sees B evs";
-by (list.induct_tac "evs" 1);
-by (agent.induct_tac "B" 1);
+by (induct_tac "evs" 1);
+by (induct_tac "B" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Auto_tac ());
 qed_spec_mp "sees_pubK";
 
 (*Spy sees private keys of agents!*)
 goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
-by (list.induct_tac "evs" 1);
+by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
 qed "Spy_sees_lost";
@@ -94,7 +94,7 @@
 (*** Fresh nonces ***)
 
 goal thy "Nonce N ~: parts (initState B)";
-by (agent.induct_tac "B" 1);
+by (induct_tac "B" 1);
 by (Auto_tac ());
 qed "Nonce_notin_initState";
 AddIffs [Nonce_notin_initState];
@@ -108,12 +108,12 @@
 (*** Supply fresh nonces for possibility theorems. ***)
 
 goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
-by (list.induct_tac "evs" 1);
+by (induct_tac "evs" 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (Step_tac 1);
 by (Full_simp_tac 1);
 (*Inductive step*)
-by (event.induct_tac "a" 1);
+by (induct_tac "a" 1);
 by (ALLGOALS (full_simp_tac 
 	      (!simpset delsimps [sees_Notes]
 		        addsimps [UN_parts_sees_Says,

--- a/src/HOL/Auth/Shared.ML	Thu Sep 11 12:21:34 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Sep 11 12:22:31 1997 +0200
@@ -23,7 +23,7 @@
     -- not in normal form! **)
 
 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
-by (agent.induct_tac "C" 1);
+by (induct_tac "C" 1);
 by (Auto_tac ());
 qed "keysFor_parts_initState";
 Addsimps [keysFor_parts_initState];
@@ -33,15 +33,15 @@
 
 (*Agents see their own shared keys!*)
 goal thy "A ~= Spy --> Key (shrK A) : sees A evs";
-by (list.induct_tac "evs" 1);
-by (agent.induct_tac "A" 1);
+by (induct_tac "evs" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
 qed_spec_mp "sees_own_shrK";
 
 (*Spy sees shared keys of agents!*)
 goal thy "!!A. A: lost ==> Key (shrK A) : sees Spy evs";
-by (list.induct_tac "evs" 1);
+by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
 by (Blast_tac 1);
 qed "Spy_sees_lost";
@@ -91,7 +91,7 @@
 (*** Fresh nonces ***)
 
 goal thy "Nonce N ~: parts (initState B)";
-by (agent.induct_tac "B" 1);
+by (induct_tac "B" 1);
 by (Auto_tac ());
 qed "Nonce_notin_initState";
 AddIffs [Nonce_notin_initState];
@@ -106,12 +106,12 @@
 
 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
 goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
-by (list.induct_tac "evs" 1);
+by (induct_tac "evs" 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (Step_tac 1);
 by (Full_simp_tac 1);
 (*Inductive step*)
-by (event.induct_tac "a" 1);
+by (induct_tac "a" 1);
 by (ALLGOALS (full_simp_tac 
 	      (!simpset delsimps [sees_Notes]
 		        addsimps [UN_parts_sees_Says,