equal
deleted
inserted
replaced
35 (*Quantifier rules*) |
35 (*Quantifier rules*) |
36 val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] |
36 val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] |
37 addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; |
37 addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; |
38 |
38 |
39 val cla_setup = Cla.map_claset (K FOL_cs); |
39 val cla_setup = Cla.map_claset (K FOL_cs); |
40 |
|
41 val case_setup = |
|
42 (Method.add_methods |
|
43 [("case_tac", Method.goal_args Args.name case_tac, |
|
44 "case_tac emulation (dynamic instantiation!)")]); |
|