1.1 --- a/src/Pure/Isar/calculation.ML	Wed Apr 14 13:26:27 2004 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Wed Apr 14 13:28:46 2004 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4        state
     1.5        |> reset_calculation
     1.6        |> Proof.reset_thms calculationN
     1.7 -      |> Proof.simple_have_thms "" calc
     1.8 +      |> Proof.simple_note_thms "" calc
     1.9        |> Proof.chain;
    1.10  
    1.11  

     2.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Apr 14 13:26:27 2004 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Apr 14 13:28:46 2004 +0200
     2.3 @@ -244,21 +244,21 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k);
     2.8 -fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc;
     2.9 +fun theorems_i k = present_thmss k oo PureThy.note_thmss_i (Drule.kind k);
    2.10 +fun locale_theorems_i k loc = present_thmss k oo Locale.note_thmss_i k loc;
    2.11  
    2.12  fun theorems k args thy = thy
    2.13 -  |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
    2.14 +  |> PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
    2.15    |> present_thmss k;
    2.16  
    2.17  fun locale_theorems k loc args thy = thy
    2.18 -  |> Locale.have_thmss k loc (local_attribs thy args)
    2.19 +  |> Locale.note_thmss k loc (local_attribs thy args)
    2.20    |> present_thmss k;
    2.21  
    2.22  fun smart_theorems k opt_loc args thy = thy
    2.23    |> (case opt_loc of
    2.24 -    None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
    2.25 -  | Some loc => Locale.have_thmss k loc (local_attribs thy args))
    2.26 +    None => PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
    2.27 +  | Some loc => Locale.note_thmss k loc (local_attribs thy args))
    2.28    |> present_thmss k;
    2.29  
    2.30  fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
    2.31 @@ -277,10 +277,10 @@
    2.32  
    2.33  fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
    2.34  
    2.35 -val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss;
    2.36 -val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i;
    2.37 -val from_facts = chain_thmss (local_thmss Proof.have_thmss);
    2.38 -val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
    2.39 +val have_facts = ProofHistory.apply o local_thmss Proof.note_thmss;
    2.40 +val have_facts_i = ProofHistory.apply o local_thmss_i Proof.note_thmss_i;
    2.41 +val from_facts = chain_thmss (local_thmss Proof.note_thmss);
    2.42 +val from_facts_i = chain_thmss (local_thmss_i Proof.note_thmss_i);
    2.43  val with_facts = chain_thmss (local_thmss Proof.with_thmss);
    2.44  val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
    2.45  
    2.46 @@ -517,7 +517,7 @@
    2.47  
    2.48  in
    2.49  
    2.50 -fun get_thmss srcs = Proof.the_facts o local_thmss Proof.have_thmss [(("", []), srcs)];
    2.51 +fun get_thmss srcs = Proof.the_facts o local_thmss Proof.note_thmss [(("", []), srcs)];
    2.52  fun get_thmss_i thms _ = thms;
    2.53  
    2.54  fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);

     3.1 --- a/src/Pure/Isar/locale.ML	Wed Apr 14 13:26:27 2004 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Wed Apr 14 13:28:46 2004 +0200
     3.3 @@ -53,13 +53,13 @@
     3.4    val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
     3.5    val add_locale_i: bool -> bstring -> expr -> context attribute element_i list
     3.6      -> theory -> theory
     3.7 -  val smart_have_thmss: string -> (string * 'a) Library.option ->
     3.8 +  val smart_note_thmss: string -> (string * 'a) Library.option ->
     3.9      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    3.10      theory -> theory * (bstring * thm list) list
    3.11 -  val have_thmss: string -> xstring ->
    3.12 +  val note_thmss: string -> xstring ->
    3.13      ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
    3.14      theory -> theory * (bstring * thm list) list
    3.15 -  val have_thmss_i: string -> string ->
    3.16 +  val note_thmss_i: string -> string ->
    3.17      ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
    3.18      theory -> theory * (bstring * thm list) list
    3.19    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
    3.20 @@ -652,7 +652,7 @@
    3.21              in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
    3.22        in ((ctxt', axs), []) end
    3.23    | activate_elem is_ext ((ctxt, axs), Notes facts) =
    3.24 -      let val (ctxt', res) = ctxt |> ProofContext.have_thmss_i facts
    3.25 +      let val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
    3.26        in ((ctxt', axs), if is_ext then res else []) end;
    3.27  
    3.28  fun activate_elems ((name, ps), elems) (ctxt, axs) =
    3.29 @@ -1195,7 +1195,7 @@
    3.30                val facts'' = map (apfst (apfst prefix_fact)) facts'
    3.31                (* add attributes *)
    3.32                val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
    3.33 -          in fst (ProofContext.have_thmss_i facts''' ctxt)
    3.34 +          in fst (ProofContext.note_thmss_i facts''' ctxt)
    3.35            end
    3.36        | inst_elem (ctxt, (Int _)) = ctxt;
    3.37  
    3.38 @@ -1260,15 +1260,15 @@
    3.39  
    3.40  in
    3.41  
    3.42 -fun have_thmss_qualified kind name args thy =
    3.43 +fun note_thmss_qualified kind name args thy =
    3.44    thy
    3.45    |> Theory.add_path (Sign.base_name name)
    3.46 -  |> PureThy.have_thmss_i (Drule.kind kind) args
    3.47 +  |> PureThy.note_thmss_i (Drule.kind kind) args
    3.48    |>> hide_bound_names (map (#1 o #1) args)
    3.49    |>> Theory.parent_path;
    3.50  
    3.51 -fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
    3.52 -  | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
    3.53 +fun smart_note_thmss kind None = PureThy.note_thmss_i (Drule.kind kind)
    3.54 +  | smart_note_thmss kind (Some (loc, _)) = note_thmss_qualified kind loc;
    3.55    (* CB: only used in Proof.finish_global. *)
    3.56  
    3.57  end;
    3.58 @@ -1282,26 +1282,26 @@
    3.59        ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
    3.60    in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end;
    3.61  
    3.62 -fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy =
    3.63 +fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
    3.64    let
    3.65      val thy_ctxt = ProofContext.init thy;
    3.66      val loc = prep_locale (Theory.sign_of thy) raw_loc;
    3.67      val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt;
    3.68      val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
    3.69      val export = ProofContext.export_standard view loc_ctxt thy_ctxt;
    3.70 -    val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
    3.71 +    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt));
    3.72      val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
    3.73    in
    3.74      thy
    3.75      |> put_facts loc args
    3.76 -    |> have_thmss_qualified kind loc args'
    3.77 +    |> note_thmss_qualified kind loc args'
    3.78    end;
    3.79  
    3.80  in
    3.81  
    3.82 -val have_thmss = gen_have_thmss intern ProofContext.get_thms;
    3.83 -val have_thmss_i = gen_have_thmss (K I) (K I);
    3.84 -  (* CB: have_thmss(_i) is the base for the Isar commands
    3.85 +val note_thmss = gen_note_thmss intern ProofContext.get_thms;
    3.86 +val note_thmss_i = gen_note_thmss (K I) (K I);
    3.87 +  (* CB: note_thmss(_i) is the base for the Isar commands
    3.88       "theorems (in loc)" and "declare (in loc)". *)
    3.89  
    3.90  fun add_thmss loc args (thy, ctxt) =
    3.91 @@ -1405,7 +1405,7 @@
    3.92            val elemss' = change_elemss axioms elemss @
    3.93              [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
    3.94          in
    3.95 -          def_thy |> have_thmss_qualified "" aname
    3.96 +          def_thy |> note_thmss_qualified "" aname
    3.97              [((introN, []), [([intro], [])])]
    3.98            |> #1 |> rpair (elemss', [statement])
    3.99          end;
   3.100 @@ -1417,7 +1417,7 @@
   3.101              thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
   3.102            val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
   3.103          in
   3.104 -          def_thy |> have_thmss_qualified "" bname
   3.105 +          def_thy |> note_thmss_qualified "" bname
   3.106              [((introN, []), [([intro], [])]),
   3.107               ((axiomsN, []), [(map Drule.standard axioms, [])])]
   3.108            |> #1 |> rpair ([cstatement], axioms)
   3.109 @@ -1455,7 +1455,7 @@
   3.110      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
   3.111    in
   3.112      pred_thy
   3.113 -    |> have_thmss_qualified "" name facts' |> #1
   3.114 +    |> note_thmss_qualified "" name facts' |> #1
   3.115      |> declare_locale name
   3.116      |> put_locale name (make_locale view (prep_expr sign raw_import)
   3.117          (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))))

     4.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 14 13:26:27 2004 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 14 13:28:46 2004 +0200
     4.3 @@ -53,10 +53,10 @@
     4.4    val match_bind_i: (term list * term) list -> state -> state
     4.5    val let_bind: (string list * string) list -> state -> state
     4.6    val let_bind_i: (term list * term) list -> state -> state
     4.7 -  val simple_have_thms: string -> thm list -> state -> state
     4.8 -  val have_thmss: ((bstring * context attribute list) *
     4.9 +  val simple_note_thms: string -> thm list -> state -> state
    4.10 +  val note_thmss: ((bstring * context attribute list) *
    4.11      (xstring * context attribute list) list) list -> state -> state
    4.12 -  val have_thmss_i: ((bstring * context attribute list) *
    4.13 +  val note_thmss_i: ((bstring * context attribute list) *
    4.14      (thm list * context attribute list) list) list -> state -> state
    4.15    val with_thmss: ((bstring * context attribute list) *
    4.16      (xstring * context attribute list) list) list -> state -> state
    4.17 @@ -511,12 +511,11 @@
    4.18  val let_bind_i = gen_bind (ProofContext.match_bind_i true);
    4.19  
    4.20  
    4.21 -(* have_thmss *)
    4.22 -(* CB: this implements "note" of the Isar/VM *)
    4.23 +(* note_thmss *)
    4.24  
    4.25  local
    4.26  
    4.27 -fun gen_have_thmss f args state =
    4.28 +fun gen_note_thmss f args state =
    4.29    state
    4.30    |> assert_forward
    4.31    |> map_context_result (f args)
    4.32 @@ -524,10 +523,10 @@
    4.33  
    4.34  in
    4.35  
    4.36 -val have_thmss = gen_have_thmss ProofContext.have_thmss;
    4.37 -val have_thmss_i = gen_have_thmss ProofContext.have_thmss_i;
    4.38 +val note_thmss = gen_note_thmss ProofContext.note_thmss;
    4.39 +val note_thmss_i = gen_note_thmss ProofContext.note_thmss_i;
    4.40  
    4.41 -fun simple_have_thms name thms = have_thmss_i [((name, []), [(thms, [])])];
    4.42 +fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
    4.43  
    4.44  end;
    4.45  
    4.46 @@ -538,12 +537,12 @@
    4.47  
    4.48  fun gen_with_thmss f args state =
    4.49    let val state' = state |> f args
    4.50 -  in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end;
    4.51 +  in state' |> simple_note_thms "" (the_facts state' @ the_facts state) end;
    4.52  
    4.53  in
    4.54  
    4.55 -val with_thmss = gen_with_thmss have_thmss;
    4.56 -val with_thmss_i = gen_with_thmss have_thmss_i;
    4.57 +val with_thmss = gen_with_thmss note_thmss;
    4.58 +val with_thmss_i = gen_with_thmss note_thmss_i;
    4.59  
    4.60  end;
    4.61  
    4.62 @@ -562,8 +561,8 @@
    4.63  
    4.64  in
    4.65  
    4.66 -val using_thmss = gen_using_thmss ProofContext.have_thmss;
    4.67 -val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
    4.68 +val using_thmss = gen_using_thmss ProofContext.note_thmss;
    4.69 +val using_thmss_i = gen_using_thmss ProofContext.note_thmss_i;
    4.70  
    4.71  end;
    4.72  
    4.73 @@ -650,7 +649,7 @@
    4.74      |> map_context (ProofContext.qualified true)
    4.75      |> assume_i assumptions
    4.76      |> map_context (ProofContext.hide_thms false qnames)
    4.77 -    |> (fn st => simple_have_thms name (the_facts st) st)
    4.78 +    |> (fn st => simple_note_thms name (the_facts st) st)
    4.79      |> map_context (ProofContext.restore_qualified (context_of state))
    4.80    end;
    4.81  
    4.82 @@ -811,7 +810,7 @@
    4.83      outer_state
    4.84      |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
    4.85      |> (fn st => Seq.map (fn res =>
    4.86 -      have_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
    4.87 +      note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
    4.88      |> (Seq.flat o Seq.map opt_solve)
    4.89      |> (Seq.flat o Seq.map after_qed)
    4.90    end;
    4.91 @@ -855,10 +854,10 @@
    4.92              if name = "" andalso null loc_atts then thy'
    4.93              else (thy', ctxt')
    4.94                |> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
    4.95 -      |> Locale.smart_have_thmss k locale_spec
    4.96 +      |> Locale.smart_note_thmss k locale_spec
    4.97          ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
    4.98        |> (fn (thy, res) => (thy, res)
    4.99 -          |>> (#1 o Locale.smart_have_thmss k locale_spec
   4.100 +          |>> (#1 o Locale.smart_note_thmss k locale_spec
   4.101              [((name, atts), [(flat (map #2 res), [])])]));
   4.102    in (theory', ((k, name), results')) end;
   4.103  

     5.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 14 13:26:27 2004 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 14 13:28:46 2004 +0200
     5.3 @@ -84,10 +84,10 @@
     5.4    val put_thms: string * thm list -> context -> context
     5.5    val put_thmss: (string * thm list) list -> context -> context
     5.6    val reset_thms: string -> context -> context
     5.7 -  val have_thmss:
     5.8 +  val note_thmss:
     5.9      ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
    5.10        context -> context * (bstring * thm list) list
    5.11 -  val have_thmss_i:
    5.12 +  val note_thmss_i:
    5.13      ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
    5.14        context -> context * (bstring * thm list) list
    5.15    val export_assume: exporter
    5.16 @@ -1035,11 +1035,11 @@
    5.17        cases, defs));
    5.18  
    5.19  
    5.20 -(* have_thmss *)
    5.21 +(* note_thmss *)
    5.22  
    5.23  local
    5.24  
    5.25 -fun gen_have_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
    5.26 +fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
    5.27    let
    5.28      fun app ((ct, ths), (th, attrs)) =
    5.29        let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
    5.30 @@ -1048,12 +1048,12 @@
    5.31      val thms = flat (rev rev_thms);
    5.32    in (ctxt' |> put_thms (name, thms), (name, thms)) end;
    5.33  
    5.34 -fun gen_have_thmss get args ctxt = foldl_map (gen_have_thss get) (ctxt, args);
    5.35 +fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args);
    5.36  
    5.37  in
    5.38  
    5.39 -val have_thmss = gen_have_thmss get_thms;
    5.40 -val have_thmss_i = gen_have_thmss (K I);
    5.41 +val note_thmss = gen_note_thmss get_thms;
    5.42 +val note_thmss_i = gen_note_thmss (K I);
    5.43  
    5.44  end;
    5.45  
    5.46 @@ -1119,7 +1119,7 @@
    5.47      val (ctxt', [(_, thms)]) =
    5.48        ctxt
    5.49        |> auto_bind_facts props
    5.50 -      |> have_thmss_i [((name, attrs), ths)];
    5.51 +      |> note_thmss_i [((name, attrs), ths)];
    5.52    in (ctxt', (cprops, (name, asms), (name, thms))) end;
    5.53  
    5.54  fun gen_assms prepp exp args ctxt =

     6.1 --- a/src/Pure/pure_thy.ML	Wed Apr 14 13:26:27 2004 +0200
     6.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 14 13:28:46 2004 +0200
     6.3 @@ -42,9 +42,9 @@
     6.4    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
     6.5    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
     6.6      -> theory * thm list list
     6.7 -  val have_thmss: theory attribute -> ((bstring * theory attribute list) *
     6.8 +  val note_thmss: theory attribute -> ((bstring * theory attribute list) *
     6.9      (xstring * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
    6.10 -  val have_thmss_i: theory attribute -> ((bstring * theory attribute list) *
    6.11 +  val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
    6.12      (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
    6.13    val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
    6.14    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    6.15 @@ -329,11 +329,11 @@
    6.16  val add_thms = gen_add_thms (name_thms true);
    6.17  
    6.18  
    6.19 -(* have_thmss(_i) *)
    6.20 +(* note_thmss(_i) *)
    6.21  
    6.22  local
    6.23  
    6.24 -fun gen_have_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
    6.25 +fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
    6.26    let
    6.27      fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
    6.28      val (thy', thms) = enter_thms (Theory.sign_of thy)
    6.29 @@ -341,13 +341,13 @@
    6.30        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
    6.31    in (thy', (bname, thms)) end;
    6.32  
    6.33 -fun gen_have_thmss get kind_att args thy =
    6.34 -  foldl_map (gen_have_thss get kind_att) (thy, args);
    6.35 +fun gen_note_thmss get kind_att args thy =
    6.36 +  foldl_map (gen_note_thss get kind_att) (thy, args);
    6.37  
    6.38  in
    6.39  
    6.40 -val have_thmss = gen_have_thmss get_thms;
    6.41 -val have_thmss_i = gen_have_thmss (K I);
    6.42 +val note_thmss = gen_note_thmss get_thms;
    6.43 +val note_thmss_i = gen_note_thmss (K I);
    6.44  
    6.45  end;
    6.46