tuned signature;
authorwenzelm
Mon Sep 30 14:17:27 2013 +0200 (2013-09-30)
changeset 539951d457fc83f5c
parent 53994 4237859c186d
child 53996 c1097679e295
tuned signature;
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:45:17 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 14:17:27 2013 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  sig
     1.5    val mk_fun_cases: Proof.context -> term -> thm
     1.6    val fun_cases: (Attrib.binding * term list) list -> local_theory ->
     1.7 -    thm list list * local_theory
     1.8 +    (string * thm list) list * local_theory
     1.9    val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
    1.10 -    thm list list * local_theory
    1.11 +    (string * thm list) list * local_theory
    1.12  end;
    1.13  
    1.14  structure Fun_Cases : FUN_CASES =
    1.15 @@ -50,14 +50,14 @@
    1.16      val facts =
    1.17        map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    1.18          args thmss;
    1.19 -  in lthy |> Local_Theory.notes facts |>> map snd end;
    1.20 +  in lthy |> Local_Theory.notes facts end;
    1.21  
    1.22  val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
    1.23  val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
    1.24  
    1.25  val _ =
    1.26    Outer_Syntax.local_theory @{command_spec "fun_cases"}
    1.27 -    "automatic derivation of simplified elimination rules for function equations"
    1.28 +    "create simplified instances of elimination rules for function equations"
    1.29      (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
    1.30  
    1.31  end;
     2.1 --- a/src/HOL/Tools/inductive.ML	Mon Sep 30 13:45:17 2013 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Mon Sep 30 14:17:27 2013 +0200
     2.3 @@ -35,9 +35,13 @@
     2.4    val inductive_forall_def: thm
     2.5    val rulify: Proof.context -> thm -> thm
     2.6    val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
     2.7 -    thm list list * local_theory
     2.8 +    (string * thm list) list * local_theory
     2.9    val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
    2.10 -    thm list list * local_theory
    2.11 +    (string * thm list) list * local_theory
    2.12 +  val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
    2.13 +    (string * thm list) list * local_theory
    2.14 +  val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
    2.15 +    (string * thm list) list * local_theory
    2.16    type inductive_flags =
    2.17      {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    2.18        no_elim: bool, no_ind: bool, skip_mono: bool}
    2.19 @@ -578,7 +582,7 @@
    2.20      val facts =
    2.21        map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    2.22          args thmss;
    2.23 -  in lthy |> Local_Theory.notes facts |>> map snd end;
    2.24 +  in lthy |> Local_Theory.notes facts end;
    2.25  
    2.26  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    2.27  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    2.28 @@ -634,7 +638,7 @@
    2.29      val facts = args |> map (fn ((a, atts), props) =>
    2.30        ((a, map (prep_att thy) atts),
    2.31          map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
    2.32 -  in lthy |> Local_Theory.notes facts |>> map snd end;
    2.33 +  in lthy |> Local_Theory.notes facts end;
    2.34  
    2.35  val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
    2.36  val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;