changeset 14156 | 2072802ab0e3 |
parent 13034 | d7bb6e4f5f82 |
child 17876 | b9c92f384109 |
--- a/src/FOL/cladata.ML Wed Aug 20 11:00:37 2003 +0200 +++ b/src/FOL/cladata.ML Wed Aug 20 11:04:17 2003 +0200 @@ -50,4 +50,9 @@ val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] addSEs [exE,alt_ex1E] addEs [allE]; -val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)]; +val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)]; + +val case_setup = + [Method.add_methods + [("case_tac", Method.goal_args Args.name case_tac, + "case_tac emulation (dynamic instantiation!)")]];