modernized setup;
authorwenzelm
Wed Oct 29 11:41:54 2014 +0100 (2014-10-29)
changeset 58815fd3f893a40ea
parent 58814 4c0ad4162cb7
child 58816 aab139c0003f
modernized setup;
src/HOL/Inductive.thy
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Inductive.thy	Wed Oct 29 11:33:29 2014 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Oct 29 11:41:54 2014 +0100
     1.3 @@ -258,7 +258,6 @@
     1.4    Collect_mono in_mono vimage_mono
     1.5  
     1.6  ML_file "Tools/inductive.ML"
     1.7 -setup Inductive.setup
     1.8  
     1.9  theorems [mono] =
    1.10    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     2.1 --- a/src/HOL/Tools/inductive.ML	Wed Oct 29 11:33:29 2014 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Oct 29 11:41:54 2014 +0100
     2.3 @@ -64,7 +64,6 @@
     2.4    val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
     2.5    val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
     2.6    val infer_intro_vars: thm -> int -> thm list -> term list list
     2.7 -  val setup: theory -> theory
     2.8  end;
     2.9  
    2.10  signature INDUCTIVE =
    2.11 @@ -276,6 +275,11 @@
    2.12      map_data (fn (infos, monos, equations) =>
    2.13        (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
    2.14  
    2.15 +val _ =
    2.16 +  Theory.setup
    2.17 +    (Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
    2.18 +      "declaration of monotonicity rule");
    2.19 +
    2.20  
    2.21  (* equations *)
    2.22  
    2.23 @@ -587,19 +591,19 @@
    2.24  val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
    2.25  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    2.26  
    2.27 -
    2.28 -val ind_cases_setup =
    2.29 -  Method.setup @{binding ind_cases}
    2.30 -    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
    2.31 -      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
    2.32 -      (fn (raw_props, fixes) => fn ctxt =>
    2.33 -        let
    2.34 -          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
    2.35 -          val props = Syntax.read_props ctxt' raw_props;
    2.36 -          val ctxt'' = fold Variable.declare_term props ctxt';
    2.37 -          val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    2.38 -        in Method.erule ctxt 0 rules end))
    2.39 -    "dynamic case analysis on predicates";
    2.40 +val _ =
    2.41 +  Theory.setup
    2.42 +    (Method.setup @{binding ind_cases}
    2.43 +      (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
    2.44 +        Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
    2.45 +        (fn (raw_props, fixes) => fn ctxt =>
    2.46 +          let
    2.47 +            val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
    2.48 +            val props = Syntax.read_props ctxt' raw_props;
    2.49 +            val ctxt'' = fold Variable.declare_term props ctxt';
    2.50 +            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    2.51 +          in Method.erule ctxt 0 rules end))
    2.52 +      "dynamic case analysis on predicates");
    2.53  
    2.54  
    2.55  (* derivation of simplified equation *)
    2.56 @@ -1142,17 +1146,7 @@
    2.57  
    2.58  
    2.59  
    2.60 -(** package setup **)
    2.61 -
    2.62 -(* setup theory *)
    2.63 -
    2.64 -val setup =
    2.65 -  ind_cases_setup #>
    2.66 -  Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
    2.67 -    "declaration of monotonicity rule";
    2.68 -
    2.69 -
    2.70 -(* outer syntax *)
    2.71 +(** outer syntax **)
    2.72  
    2.73  fun gen_ind_decl mk_def coind =
    2.74    Parse.fixes -- Parse.for_fixes --