equal
deleted
inserted
replaced
85 |
85 |
86 (* method *) |
86 (* method *) |
87 |
87 |
88 type method = thm list -> cases_tactic; |
88 type method = thm list -> cases_tactic; |
89 |
89 |
90 fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); |
90 fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); |
91 fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); |
91 fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); |
92 |
92 |
93 val fail = METHOD (K no_tac); |
93 val fail = METHOD (K no_tac); |
94 val succeed = METHOD (K all_tac); |
94 val succeed = METHOD (K all_tac); |
95 |
95 |
96 |
96 |