# HG changeset patch
# User wenzelm
# Date 1408188230 -7200
# Node ID 75724d71013c77dc0787663000ea7f09cd98bbd1
# Parent  189d421ca72d4baba8ff550e52c4f59a09171496
modernized module name and setup;

diff -r 189d421ca72d -r 75724d71013c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Aug 16 12:15:56 2014 +0200
+++ b/src/FOL/IFOL.thy	Sat Aug 16 13:23:50 2014 +0200
@@ -710,16 +710,14 @@
 
 subsection {* Atomizing elimination rules *}
 
-setup AtomizeElim.setup
-
 lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
-by rule iprover+
+  by rule iprover+
 
 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
-by rule iprover+
+  by rule iprover+
 
 lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
-by rule iprover+
+  by rule iprover+
 
 lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
 
diff -r 189d421ca72d -r 75724d71013c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Aug 16 12:15:56 2014 +0200
+++ b/src/HOL/HOL.thy	Sat Aug 16 13:23:50 2014 +0200
@@ -763,8 +763,6 @@
 
 subsubsection {* Atomizing elimination rules *}
 
-setup AtomizeElim.setup
-
 lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
   by rule iprover+
 
diff -r 189d421ca72d -r 75724d71013c src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 12:15:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 13:23:50 2014 +0200
@@ -129,7 +129,7 @@
     | Blast_Method => blast_tac ctxt
     | Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     | Auto_Choice_Method =>
-      AtomizeElim.atomize_elim_tac ctxt THEN'
+      Atomize_Elim.atomize_elim_tac ctxt THEN'
       SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice}))
     | Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     | Linarith_Method =>
diff -r 189d421ca72d -r 75724d71013c src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sat Aug 16 12:15:56 2014 +0200
+++ b/src/Tools/atomize_elim.ML	Sat Aug 16 13:23:50 2014 +0200
@@ -6,17 +6,13 @@
 
 signature ATOMIZE_ELIM =
 sig
-  val declare_atomize_elim : attribute  
-
+  val declare_atomize_elim : attribute
   val atomize_elim_conv : Proof.context -> conv
   val full_atomize_elim_conv : Proof.context -> conv
-
   val atomize_elim_tac : Proof.context -> int -> tactic
-
-  val setup : theory -> theory
 end
 
-structure AtomizeElim : ATOMIZE_ELIM =
+structure Atomize_Elim : ATOMIZE_ELIM =
 struct
 
 (* theory data *)
@@ -27,6 +23,8 @@
   val description = "atomize_elim rewrite rule";
 );
 
+val _ = Theory.setup AtomizeElimData.setup;
+
 val declare_atomize_elim = AtomizeElimData.add
 
 (* More conversions: *)
@@ -50,7 +48,7 @@
     in Thm.equal_intr fwd back end
 
 
-(* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
+(* convert !!thesis. (!!x y z. ... => thesis) ==> ...
                      ==> (!!a b c. ... => thesis)
                      ==> thesis
 
@@ -71,7 +69,7 @@
 fun thesis_miniscope_conv inner_cv ctxt =
     let
       (* check if the outermost quantifier binds the conclusion *)
-      fun is_forall_thesis t = 
+      fun is_forall_thesis t =
           case Logic.strip_assums_concl t of
             (_ $ Bound i) => i = length (Logic.strip_params t) - 1
           | _ => false
@@ -93,11 +91,11 @@
           end
 
       (* move current quantifier to the right *)
-      fun moveq_conv ctxt = 
+      fun moveq_conv ctxt =
           (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
           else_conv (movea_conv ctxt)
 
-      fun ms_conv ctxt ct = 
+      fun ms_conv ctxt ct =
           if is_forall_thesis (term_of ct)
           then moveq_conv ctxt ct
           else (implies_concl_conv (ms_conv ctxt)
@@ -105,7 +103,7 @@
             (forall_conv (ms_conv o snd) ctxt))
             ct
     in
-      ms_conv ctxt 
+      ms_conv ctxt
     end
 
 val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
@@ -117,13 +115,13 @@
     let
       val thy = Proof_Context.theory_of ctxt
       val _ $ thesis = Logic.strip_assums_concl subg
-                       
+
       (* Introduce a quantifier first if the thesis is not bound *)
-      val quantify_thesis = 
+      val quantify_thesis =
           if is_Bound thesis then all_tac
           else let
               val cthesis = cterm_of thy thesis
-              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
+              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
                          @{thm meta_spec}
             in
               compose_tac (false, rule, 1) i
@@ -133,9 +131,9 @@
       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
     end)
 
-val setup =
-  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
-    "convert obtains statement to atomic object logic goal"
-  #> AtomizeElimData.setup
+val _ =
+  Theory.setup
+    (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
+      "convert obtains statement to atomic object logic goal")
 
 end