--- a/src/HOL/TLA/Inc/Inc.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML Wed Dec 24 10:02:30 1997 +0100
@@ -171,7 +171,7 @@
(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,
- Auto_tac()
+ Auto_tac
]);
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
@@ -217,7 +217,7 @@
(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,
- Auto_tac()
+ Auto_tac
]);
qed_goal "N1_enabled_at_b" Inc.thy