method brute_force = ALLGOALS force_tac;
authorwenzelm
Sun Nov 29 13:13:57 1998 +0100 (1998-11-29)
changeset 59859481d0cfb86e
parent 5984 4c2fc177f4d3
child 5986 6ebbc9e7cc20
method brute_force = ALLGOALS force_tac;
src/Provers/clasimp.ML
     1.1 --- a/src/Provers/clasimp.ML	Fri Nov 27 17:01:21 1998 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Sun Nov 29 13:13:57 1998 +0100
     1.3 @@ -165,7 +165,8 @@
     1.4   [Method.add_methods
     1.5     [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"),
     1.6      ("auto", clasimp_method auto_tac, "auto"),
     1.7 -    ("force", clasimp_method' force_tac, "force")]];
     1.8 +    ("force", clasimp_method' force_tac, "force"),
     1.9 +    ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];
    1.10  
    1.11  
    1.12  end;