equal
deleted
inserted
replaced
13 "methods" |
13 "methods" |
14 "\<bar>" "\<Rightarrow>" |
14 "\<bar>" "\<Rightarrow>" |
15 "uses" |
15 "uses" |
16 begin |
16 begin |
17 |
17 |
18 ML_file "parse_tools.ML" |
18 ML_file \<open>parse_tools.ML\<close> |
19 ML_file "method_closure.ML" |
19 ML_file \<open>method_closure.ML\<close> |
20 ML_file "eisbach_rule_insts.ML" |
20 ML_file \<open>eisbach_rule_insts.ML\<close> |
21 ML_file "match_method.ML" |
21 ML_file \<open>match_method.ML\<close> |
22 |
22 |
23 |
23 |
24 method solves methods m = (m; fail) |
24 method solves methods m = (m; fail) |
25 |
25 |
26 method repeat_new methods m = (m ; (repeat_new \<open>m\<close>)?) |
26 method repeat_new methods m = (m ; (repeat_new \<open>m\<close>)?) |