equal
deleted
inserted
replaced
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 |
22 |
23 method solves methods m = (m; fail) |
23 method solves methods m = (m; fail) |
24 |
24 |
25 method_setup use = \<open> |
|
26 Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >> |
|
27 (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms) |
|
28 \<close> \<open>indicate method facts and context for method expression\<close> |
|
29 |
|
30 end |
25 end |