src/HOL/TLA/Action.ML
changeset 6301 08245f5a436d
parent 6255 db63752140c7
child 7881 1b1db39a110b
     1.1 --- a/src/HOL/TLA/Action.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/TLA/Action.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -253,6 +253,6 @@
     1.4  
     1.5  val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
     1.6  by (enabled_tac prem 1);
     1.7 -auto();
     1.8 +by Auto_tac;
     1.9  
    1.10  *)