--- a/src/HOL/Eisbach/Eisbach.thy Sun May 03 18:45:58 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Sun May 03 18:51:26 2015 +0200
@@ -1,11 +1,11 @@
-(* Title: Eisbach.thy
+(* Title: HOL/Eisbach/Eisbach.thy
Author: Daniel Matichuk, NICTA/UNSW
Main entry point for Eisbach proof method language.
*)
theory Eisbach
-imports Pure
+imports Main
keywords
"method" :: thy_decl and
"conclusion"
@@ -16,7 +16,6 @@
"uses"
begin
-
ML_file "parse_tools.ML"
ML_file "eisbach_rule_insts.ML"
ML_file "method_closure.ML"
@@ -24,20 +23,12 @@
ML_file "eisbach_antiquotations.ML"
(* FIXME reform Isabelle/Pure attributes to make this work by default *)
-attribute_setup THEN =
- \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) =>
- Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
- "resolution with rule"
-
-attribute_setup OF =
- \<open>Attrib.thms >> (fn Bs =>
- Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
- "rule resolved with facts"
-
-attribute_setup rotated =
- \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n =>
- Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
- "rotated theorem premises"
+setup \<open>
+ fold (Method_Closure.wrap_attribute true)
+ [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
+ fold (Method_Closure.wrap_attribute false)
+ [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
+\<close>
method solves methods m = (m; fail)