grouped versions of axioms/define/notes;
authorwenzelm
Sat Jan 26 17:08:43 2008 +0100 (2008-01-26)
changeset 25984da0399c9ffcb
parent 25983 111d2ed164f4
child 25985 8d69087f6a4b
grouped versions of axioms/define/notes;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Jan 26 17:08:42 2008 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Jan 26 17:08:43 2008 +0100
     1.3 @@ -24,17 +24,29 @@
     1.4    val axioms: string ->
     1.5      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     1.6      -> (term list * (bstring * thm list) list) * local_theory
     1.7 +  val axioms_grouped: string -> string ->
     1.8 +    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     1.9 +    -> (term list * (bstring * thm list) list) * local_theory
    1.10    val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    1.11      (term * term) * local_theory
    1.12    val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.13      (term * (bstring * thm)) * local_theory
    1.14 +  val define_grouped: string -> string ->
    1.15 +    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.16 +    (term * (bstring * thm)) * local_theory
    1.17 +  val note: string -> (bstring * Attrib.src list) * thm list ->
    1.18 +    local_theory -> (bstring * thm list) * local_theory
    1.19    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.20      local_theory -> (bstring * thm list) list * local_theory
    1.21 +  val note_grouped: string -> string ->
    1.22 +    (bstring * Attrib.src list) * thm list ->
    1.23 +    local_theory -> (bstring * thm list) * local_theory
    1.24 +  val notes_grouped: string -> string ->
    1.25 +    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.26 +    local_theory -> (bstring * thm list) list * local_theory
    1.27    val type_syntax: declaration -> local_theory -> local_theory
    1.28    val term_syntax: declaration -> local_theory -> local_theory
    1.29    val declaration: declaration -> local_theory -> local_theory
    1.30 -  val note: string -> (bstring * Attrib.src list) * thm list ->
    1.31 -    local_theory -> (bstring * thm list) * local_theory
    1.32    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.33    val target_morphism: local_theory -> morphism
    1.34    val init: string -> operations -> Proof.context -> local_theory
    1.35 @@ -52,13 +64,14 @@
    1.36  
    1.37  type operations =
    1.38   {pretty: local_theory -> Pretty.T list,
    1.39 -  axioms: string ->
    1.40 +  axioms: string -> string ->
    1.41      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    1.42      -> (term list * (bstring * thm list) list) * local_theory,
    1.43    abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
    1.44 -  define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.45 +  define: string -> string ->
    1.46 +    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    1.47      (term * (bstring * thm)) * local_theory,
    1.48 -  notes: string ->
    1.49 +  notes: string -> string ->
    1.50      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.51      local_theory -> (bstring * thm list) list * local_theory,
    1.52    type_syntax: declaration -> local_theory -> local_theory,
    1.53 @@ -144,17 +157,24 @@
    1.54  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    1.55  fun operation1 f x = operation (fn ops => f ops x);
    1.56  fun operation2 f x y = operation (fn ops => f ops x y);
    1.57 +fun operation3 f x y z = operation (fn ops => f ops x y z);
    1.58  
    1.59  val pretty = operation #pretty;
    1.60 -val axioms = operation2 #axioms;
    1.61 +val axioms_grouped = operation3 #axioms;
    1.62  val abbrev = operation2 #abbrev;
    1.63 -val define = operation2 #define;
    1.64 -val notes = operation2 #notes;
    1.65 +val define_grouped = operation3 #define;
    1.66 +val notes_grouped = operation3 #notes;
    1.67  val type_syntax = operation1 #type_syntax;
    1.68  val term_syntax = operation1 #term_syntax;
    1.69  val declaration = operation1 #declaration;
    1.70  
    1.71 -fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
    1.72 +fun note_grouped kind group (a, ths) lthy = lthy
    1.73 +  |> notes_grouped kind group [(a, [(ths, [])])] |>> the_single;
    1.74 +
    1.75 +fun axioms kind = axioms_grouped kind "";
    1.76 +fun define kind = define_grouped kind "";
    1.77 +fun notes kind = notes_grouped kind "";
    1.78 +fun note kind = note_grouped kind "";
    1.79  
    1.80  fun target_morphism lthy =
    1.81    ProofContext.export_morphism lthy (target_of lthy) $>
     2.1 --- a/src/Pure/Isar/theory_target.ML	Sat Jan 26 17:08:42 2008 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Jan 26 17:08:43 2008 +0100
     2.3 @@ -150,7 +150,7 @@
     2.4    |> ProofContext.note_thmss_i kind facts
     2.5    ||> ProofContext.restore_naming ctxt;
     2.6  
     2.7 -fun notes (Target {target, is_locale, ...}) kind facts lthy =
     2.8 +fun notes (Target {target, is_locale, ...}) kind group facts lthy =
     2.9    let
    2.10      val thy = ProofContext.theory_of lthy;
    2.11      val full = LocalTheory.full_name lthy;
    2.12 @@ -167,7 +167,7 @@
    2.13    in
    2.14      lthy |> LocalTheory.theory
    2.15        (Sign.qualified_names
    2.16 -        #> PureThy.note_thmss_i kind global_facts #> snd
    2.17 +        #> PureThy.note_thmss_grouped kind group global_facts #> snd
    2.18          #> Sign.restore_naming thy)
    2.19  
    2.20      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    2.21 @@ -265,7 +265,7 @@
    2.22  (* define *)
    2.23  
    2.24  fun define (ta as Target {target, is_locale, is_class, ...})
    2.25 -    kind ((c, mx), ((name, atts), rhs)) lthy =
    2.26 +    kind group ((c, mx), ((name, atts), rhs)) lthy =
    2.27    let
    2.28      val thy = ProofContext.theory_of lthy;
    2.29      val thy_ctxt = ProofContext.init thy;
    2.30 @@ -296,13 +296,13 @@
    2.31  
    2.32      (*note*)
    2.33      val ([(res_name, [res])], lthy4) = lthy3
    2.34 -      |> notes ta kind [((name', atts), [([def], [])])];
    2.35 +      |> notes ta kind group [((name', atts), [([def], [])])];
    2.36    in ((lhs, (res_name, res)), lthy4) end;
    2.37  
    2.38  
    2.39  (* axioms *)
    2.40  
    2.41 -fun axioms ta kind (vars, specs) lthy =
    2.42 +fun axioms ta kind group (vars, specs) lthy =
    2.43    let
    2.44      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    2.45      val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
    2.46 @@ -322,7 +322,7 @@
    2.47      |> fold Variable.declare_term expanded_props
    2.48      |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
    2.49      |> LocalTheory.theory_result (fold_map axiom specs)
    2.50 -    |-> notes ta kind
    2.51 +    |-> notes ta kind group
    2.52      |>> pair (map #1 consts)
    2.53    end;
    2.54