equal
deleted
inserted
replaced
19 ML_file "method_closure.ML" |
19 ML_file "method_closure.ML" |
20 ML_file "eisbach_rule_insts.ML" |
20 ML_file "eisbach_rule_insts.ML" |
21 ML_file "match_method.ML" |
21 ML_file "match_method.ML" |
22 ML_file "eisbach_antiquotations.ML" |
22 ML_file "eisbach_antiquotations.ML" |
23 |
23 |
24 (* FIXME reform Isabelle/Pure attributes to make this work by default *) |
|
25 setup \<open> |
|
26 fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true}) |
|
27 [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #> |
|
28 fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false}) |
|
29 [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}] |
|
30 \<close> |
|
31 |
|
32 method solves methods m = (m; fail) |
24 method solves methods m = (m; fail) |
33 |
25 |
34 end |
26 end |