--- a/src/HOL/Eisbach/Eisbach.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Thu Apr 30 17:02:57 2015 +0200
@@ -8,14 +8,15 @@
imports Pure
keywords
"method" :: thy_decl and
- "concl"
- "prems" (* FIXME conflict with "prems" in Isar, which is presently dormant *)
+ "conclusion"
+ "premises"
"declares"
"methods"
"\<bar>" "\<Rightarrow>"
"uses"
begin
+
ML_file "parse_tools.ML"
ML_file "eisbach_rule_insts.ML"
ML_file "method_closure.ML"
@@ -38,6 +39,6 @@
Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
"rotated theorem premises"
-method solves methods m = \<open>m; fail\<close>
+method solves methods m = (m; fail)
end