# HG changeset patch
# User nipkow
# Date 901260604 -7200
# Node ID 36d38be7e814329188248b78db98a9bc7958ae58
# Parent  2dbef0104bcf2724a23c7003bb1d4f7dc64862af
induct_tac -> exhaust_tac in 2 places.

diff -r 2dbef0104bcf -r 36d38be7e814 src/HOL/TLA/Inc/Inc.ML
--- a/src/HOL/TLA/Inc/Inc.ML	Wed Jul 22 17:59:49 1998 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML	Fri Jul 24 08:10:04 1998 +0200
@@ -170,7 +170,7 @@
 \  .-> <>($pc2 .= #a)"
   (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
 	    rewrite_goals_tac (Init_def::action_rews),
-	    pcount.induct_tac "pc2 (fst_st sigma)" 1,
+	    exhaust_tac "pc2 (fst_st sigma)" 1,
 	    Auto_tac
 	   ]);
 
@@ -216,7 +216,7 @@
 \  .-> <>($pc1 .= #b)"
   (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
 	    rewrite_goals_tac (Init_def::action_rews),
-	    pcount.induct_tac "pc1 (fst_st sigma)" 1,
+	    exhaust_tac "pc1 (fst_st sigma)" 1,
 	    Auto_tac
 	   ]);