add_defs(_i): overloaded option;
authorwenzelm
Thu Jul 13 23:14:49 2000 +0200 (2000-07-13)
changeset 93184c3fb0786022
parent 9317 7a72952ca068
child 9319 488e0367a77d
add_defs(_i): overloaded option;
src/Pure/Isar/isar_thy.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Jul 13 23:14:15 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 13 23:14:49 2000 +0200
     1.3 @@ -51,8 +51,9 @@
     1.4    val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
     1.5    val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
     1.6      -> theory -> theory
     1.7 -  val add_defs: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
     1.8 -  val add_defs_i: (((bstring * term) * theory attribute list) * Comment.text) list
     1.9 +  val add_defs: bool * (((bstring * string) * Args.src list) * Comment.text) list
    1.10 +    -> theory -> theory
    1.11 +  val add_defs_i: bool * (((bstring * term) * theory attribute list) * Comment.text) list
    1.12      -> theory -> theory
    1.13    val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list
    1.14      -> theory -> theory
    1.15 @@ -263,8 +264,8 @@
    1.16  
    1.17  val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
    1.18  val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
    1.19 -val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore;
    1.20 -val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore;
    1.21 +fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) (map Comment.ignore args);
    1.22 +fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) (map Comment.ignore args);
    1.23  
    1.24  
    1.25  (* constdefs *)
    1.26 @@ -272,7 +273,7 @@
    1.27  fun gen_add_constdefs consts defs args thy =
    1.28    thy
    1.29    |> consts (map (Comment.ignore o fst) args)
    1.30 -  |> defs (map (fn (((c, _, mx), _), (s, _)) =>
    1.31 +  |> defs (false, map (fn (((c, _, mx), _), (s, _)) =>
    1.32      (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args);
    1.33  
    1.34  fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args;
     2.1 --- a/src/Pure/pure_thy.ML	Thu Jul 13 23:14:15 2000 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Thu Jul 13 23:14:49 2000 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  (*  Title:      Pure/pure_thy.ML
     2.5      ID:         $Id$
     2.6      Author:     Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  Theorem database, derived theory operations, and the ProtoPure theory.
    2.10  *)
    2.11 @@ -38,10 +39,14 @@
    2.12    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    2.13    val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
    2.14    val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
    2.15 -  val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
    2.16 -  val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    2.17 -  val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
    2.18 -  val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
    2.19 +  val add_defs: bool -> ((bstring * string) * theory attribute list) list
    2.20 +    -> theory -> theory * thm list
    2.21 +  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
    2.22 +    -> theory -> theory * thm list
    2.23 +  val add_defss: bool -> ((bstring * string list) * theory attribute list) list
    2.24 +    -> theory -> theory * thm list list
    2.25 +  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list
    2.26 +    -> theory -> theory * thm list list
    2.27    val get_name: theory -> string
    2.28    val put_name: string -> theory -> theory
    2.29    val global_path: theory -> theory
    2.30 @@ -323,10 +328,10 @@
    2.31    val add_axioms_i  = add_singles Theory.add_axioms_i;
    2.32    val add_axiomss   = add_multis Theory.add_axioms;
    2.33    val add_axiomss_i = add_multis Theory.add_axioms_i;
    2.34 -  val add_defs      = add_singles Theory.add_defs;
    2.35 -  val add_defs_i    = add_singles Theory.add_defs_i;
    2.36 -  val add_defss     = add_multis Theory.add_defs;
    2.37 -  val add_defss_i   = add_multis Theory.add_defs_i;
    2.38 +  val add_defs      = add_singles o Theory.add_defs;
    2.39 +  val add_defs_i    = add_singles o Theory.add_defs_i;
    2.40 +  val add_defss     = add_multis o Theory.add_defs;
    2.41 +  val add_defss_i   = add_multis o Theory.add_defs_i;
    2.42  end;
    2.43  
    2.44  
    2.45 @@ -451,7 +456,7 @@
    2.46    |> Theory.add_modesyntax ("", false)
    2.47      [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
    2.48    |> local_path
    2.49 -  |> (#1 oo (add_defs o map Thm.no_attributes))
    2.50 +  |> (#1 oo (add_defs false o map Thm.no_attributes))
    2.51     [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
    2.52      ("Goal_def", "GOAL (PROP A) == PROP A")]
    2.53    |> (#1 o add_thmss [(("nothing", []), [])])