--- a/src/HOL/TLA/Inc/Inc.ML Mon Mar 13 15:42:19 2000 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML Mon Mar 13 16:23:34 2000 +0100
@@ -165,7 +165,7 @@
(fn _ => [auto_tac (Inc_css addsimps2 Init_defs
addSIs2 [(temp_use N2_leadsto_a)
RSN(2, (temp_use leadsto_init))]),
- cases_tac "pc2 (st1 sigma)" 1,
+ case_tac "pc2 (st1 sigma)" 1,
Auto_tac
]);
@@ -212,7 +212,7 @@
(fn _ => [auto_tac (Inc_css addsimps2 Init_defs
addSIs2 [(temp_use N1_leadsto_b)
RSN(2, temp_use leadsto_init)]),
- cases_tac "pc1 (st1 sigma)" 1,
+ case_tac "pc1 (st1 sigma)" 1,
Auto_tac
]);