src/HOL/TLA/Inc/Inc.ML
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/TLA/Inc/Inc.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/Inc/Inc.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4    (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
     1.5  	    rewrite_goals_tac (Init_def::action_rews),
     1.6  	    pcount.induct_tac "pc2 (fst_st sigma)" 1,
     1.7 -	    Auto_tac()
     1.8 +	    Auto_tac
     1.9  	   ]);
    1.10  
    1.11  (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
    1.12 @@ -217,7 +217,7 @@
    1.13    (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
    1.14  	    rewrite_goals_tac (Init_def::action_rews),
    1.15  	    pcount.induct_tac "pc1 (fst_st sigma)" 1,
    1.16 -	    Auto_tac()
    1.17 +	    Auto_tac
    1.18  	   ]);
    1.19  
    1.20  qed_goal "N1_enabled_at_b" Inc.thy