src/HOL/TLA/Action.ML
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 6255 db63752140c7
     1.1 --- a/src/HOL/TLA/Action.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/Action.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -219,17 +219,17 @@
     1.4  
     1.5  qed_goalw "idle_squareI" Action.thy [square_def]
     1.6     "!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)"
     1.7 -   (fn _ => [ Auto_tac() ]);
     1.8 +   (fn _ => [ Auto_tac ]);
     1.9  
    1.10  qed_goalw "busy_squareI" Action.thy [square_def]
    1.11     "!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)"
    1.12 -   (fn _ => [ Auto_tac() ]);
    1.13 +   (fn _ => [ Auto_tac ]);
    1.14  
    1.15  qed_goalw "square_simulation" Action.thy [square_def]
    1.16     "[| unchanged f .& .~B .-> unchanged g;   \
    1.17  \      A .& .~unchanged g .-> B              \
    1.18  \   |] ==> [A]_f .-> [B]_g"
    1.19 -   (fn [p1,p2] => [Auto_tac(),
    1.20 +   (fn [p1,p2] => [Auto_tac,
    1.21                     etac (action_conjimpE p2) 1,
    1.22                     etac swap 3, etac (action_conjimpE p1) 3,
    1.23                     ALLGOALS atac
    1.24 @@ -237,11 +237,11 @@
    1.25                     
    1.26  qed_goalw "not_square" Action.thy [square_def,angle_def]
    1.27     "(.~ [A]_v) .= <.~A>_v"
    1.28 -   (fn _ => [ Auto_tac() ]);
    1.29 +   (fn _ => [ Auto_tac ]);
    1.30  
    1.31  qed_goalw "not_angle" Action.thy [square_def,angle_def]
    1.32     "(.~ <A>_v) .= [.~A]_v"
    1.33 -   (fn _ => [ Auto_tac() ]);
    1.34 +   (fn _ => [ Auto_tac ]);
    1.35  
    1.36  (* ============================== Facts about ENABLED ============================== *)
    1.37  
    1.38 @@ -278,22 +278,22 @@
    1.39  
    1.40  qed_goal "enabled_disj1" Action.thy
    1.41    "!!s. (Enabled F) s ==> (Enabled (F .| G)) s"
    1.42 -  (fn _ => [etac enabled_mono 1, Auto_tac()
    1.43 +  (fn _ => [etac enabled_mono 1, Auto_tac
    1.44  	   ]);
    1.45  
    1.46  qed_goal "enabled_disj2" Action.thy
    1.47    "!!s. (Enabled G) s ==> (Enabled (F .| G)) s"
    1.48 -  (fn _ => [etac enabled_mono 1, Auto_tac()
    1.49 +  (fn _ => [etac enabled_mono 1, Auto_tac
    1.50  	   ]);
    1.51  
    1.52  qed_goal "enabled_conj1" Action.thy
    1.53    "!!s. (Enabled (F .& G)) s ==> (Enabled F) s"
    1.54 -  (fn _ => [etac enabled_mono 1, Auto_tac()
    1.55 +  (fn _ => [etac enabled_mono 1, Auto_tac
    1.56             ]);
    1.57  
    1.58  qed_goal "enabled_conj2" Action.thy
    1.59    "!!s. (Enabled (F .& G)) s ==> (Enabled G) s"
    1.60 -  (fn _ => [etac enabled_mono 1, Auto_tac()
    1.61 +  (fn _ => [etac enabled_mono 1, Auto_tac
    1.62             ]);
    1.63  
    1.64  qed_goal "enabled_conjE" Action.thy