# HG changeset patch
# User wenzelm
# Date 1081942126 -7200
# Node ID 3667b4616e9ab0c76d59e3e370a2d8e1ab00003a
# Parent  4bf2d10461f3ebad180423df86c5d47e74e2f828
renamed have_thms to note_thms;

diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -150,7 +150,7 @@
       state
       |> reset_calculation
       |> Proof.reset_thms calculationN
-      |> Proof.simple_have_thms "" calc
+      |> Proof.simple_note_thms "" calc
       |> Proof.chain;
 
 
diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -244,21 +244,21 @@
 
 in
 
-fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k);
-fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc;
+fun theorems_i k = present_thmss k oo PureThy.note_thmss_i (Drule.kind k);
+fun locale_theorems_i k loc = present_thmss k oo Locale.note_thmss_i k loc;
 
 fun theorems k args thy = thy
-  |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
+  |> PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
   |> present_thmss k;
 
 fun locale_theorems k loc args thy = thy
-  |> Locale.have_thmss k loc (local_attribs thy args)
+  |> Locale.note_thmss k loc (local_attribs thy args)
   |> present_thmss k;
 
 fun smart_theorems k opt_loc args thy = thy
   |> (case opt_loc of
-    None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
-  | Some loc => Locale.have_thmss k loc (local_attribs thy args))
+    None => PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
+  | Some loc => Locale.note_thmss k loc (local_attribs thy args))
   |> present_thmss k;
 
 fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
@@ -277,10 +277,10 @@
 
 fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
 
-val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss;
-val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i;
-val from_facts = chain_thmss (local_thmss Proof.have_thmss);
-val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
+val have_facts = ProofHistory.apply o local_thmss Proof.note_thmss;
+val have_facts_i = ProofHistory.apply o local_thmss_i Proof.note_thmss_i;
+val from_facts = chain_thmss (local_thmss Proof.note_thmss);
+val from_facts_i = chain_thmss (local_thmss_i Proof.note_thmss_i);
 val with_facts = chain_thmss (local_thmss Proof.with_thmss);
 val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
 
@@ -517,7 +517,7 @@
 
 in
 
-fun get_thmss srcs = Proof.the_facts o local_thmss Proof.have_thmss [(("", []), srcs)];
+fun get_thmss srcs = Proof.the_facts o local_thmss Proof.note_thmss [(("", []), srcs)];
 fun get_thmss_i thms _ = thms;
 
 fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);
diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -53,13 +53,13 @@
   val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
   val add_locale_i: bool -> bstring -> expr -> context attribute element_i list
     -> theory -> theory
-  val smart_have_thmss: string -> (string * 'a) Library.option ->
+  val smart_note_thmss: string -> (string * 'a) Library.option ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val have_thmss: string -> xstring ->
+  val note_thmss: string -> xstring ->
     ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
-  val have_thmss_i: string -> string ->
+  val note_thmss_i: string -> string ->
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   val add_thmss: string -> ((string * thm list) * context attribute list) list ->
@@ -652,7 +652,7 @@
             in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
       in ((ctxt', axs), []) end
   | activate_elem is_ext ((ctxt, axs), Notes facts) =
-      let val (ctxt', res) = ctxt |> ProofContext.have_thmss_i facts
+      let val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
       in ((ctxt', axs), if is_ext then res else []) end;
 
 fun activate_elems ((name, ps), elems) (ctxt, axs) =
@@ -1195,7 +1195,7 @@
               val facts'' = map (apfst (apfst prefix_fact)) facts'
               (* add attributes *)
               val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
-          in fst (ProofContext.have_thmss_i facts''' ctxt)
+          in fst (ProofContext.note_thmss_i facts''' ctxt)
           end
       | inst_elem (ctxt, (Int _)) = ctxt;
 
@@ -1260,15 +1260,15 @@
 
 in
 
-fun have_thmss_qualified kind name args thy =
+fun note_thmss_qualified kind name args thy =
   thy
   |> Theory.add_path (Sign.base_name name)
-  |> PureThy.have_thmss_i (Drule.kind kind) args
+  |> PureThy.note_thmss_i (Drule.kind kind) args
   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
 
-fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
-  | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
+fun smart_note_thmss kind None = PureThy.note_thmss_i (Drule.kind kind)
+  | smart_note_thmss kind (Some (loc, _)) = note_thmss_qualified kind loc;
   (* CB: only used in Proof.finish_global. *)
 
 end;
@@ -1282,26 +1282,26 @@
       ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
   in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end;
 
-fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy =
+fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   let
     val thy_ctxt = ProofContext.init thy;
     val loc = prep_locale (Theory.sign_of thy) raw_loc;
     val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt;
     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
     val export = ProofContext.export_standard view loc_ctxt thy_ctxt;
-    val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
+    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt));
     val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   in
     thy
     |> put_facts loc args
-    |> have_thmss_qualified kind loc args'
+    |> note_thmss_qualified kind loc args'
   end;
 
 in
 
-val have_thmss = gen_have_thmss intern ProofContext.get_thms;
-val have_thmss_i = gen_have_thmss (K I) (K I);
-  (* CB: have_thmss(_i) is the base for the Isar commands
+val note_thmss = gen_note_thmss intern ProofContext.get_thms;
+val note_thmss_i = gen_note_thmss (K I) (K I);
+  (* CB: note_thmss(_i) is the base for the Isar commands
      "theorems (in loc)" and "declare (in loc)". *)
 
 fun add_thmss loc args (thy, ctxt) =
@@ -1405,7 +1405,7 @@
           val elemss' = change_elemss axioms elemss @
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
-          def_thy |> have_thmss_qualified "" aname
+          def_thy |> note_thmss_qualified "" aname
             [((introN, []), [([intro], [])])]
           |> #1 |> rpair (elemss', [statement])
         end;
@@ -1417,7 +1417,7 @@
             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
           val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
         in
-          def_thy |> have_thmss_qualified "" bname
+          def_thy |> note_thmss_qualified "" bname
             [((introN, []), [([intro], [])]),
              ((axiomsN, []), [(map Drule.standard axioms, [])])]
           |> #1 |> rpair ([cstatement], axioms)
@@ -1455,7 +1455,7 @@
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
   in
     pred_thy
-    |> have_thmss_qualified "" name facts' |> #1
+    |> note_thmss_qualified "" name facts' |> #1
     |> declare_locale name
     |> put_locale name (make_locale view (prep_expr sign raw_import)
         (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))))
diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -53,10 +53,10 @@
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
-  val simple_have_thms: string -> thm list -> state -> state
-  val have_thmss: ((bstring * context attribute list) *
+  val simple_note_thms: string -> thm list -> state -> state
+  val note_thmss: ((bstring * context attribute list) *
     (xstring * context attribute list) list) list -> state -> state
-  val have_thmss_i: ((bstring * context attribute list) *
+  val note_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
   val with_thmss: ((bstring * context attribute list) *
     (xstring * context attribute list) list) list -> state -> state
@@ -511,12 +511,11 @@
 val let_bind_i = gen_bind (ProofContext.match_bind_i true);
 
 
-(* have_thmss *)
-(* CB: this implements "note" of the Isar/VM *)
+(* note_thmss *)
 
 local
 
-fun gen_have_thmss f args state =
+fun gen_note_thmss f args state =
   state
   |> assert_forward
   |> map_context_result (f args)
@@ -524,10 +523,10 @@
 
 in
 
-val have_thmss = gen_have_thmss ProofContext.have_thmss;
-val have_thmss_i = gen_have_thmss ProofContext.have_thmss_i;
+val note_thmss = gen_note_thmss ProofContext.note_thmss;
+val note_thmss_i = gen_note_thmss ProofContext.note_thmss_i;
 
-fun simple_have_thms name thms = have_thmss_i [((name, []), [(thms, [])])];
+fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
 
 end;
 
@@ -538,12 +537,12 @@
 
 fun gen_with_thmss f args state =
   let val state' = state |> f args
-  in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end;
+  in state' |> simple_note_thms "" (the_facts state' @ the_facts state) end;
 
 in
 
-val with_thmss = gen_with_thmss have_thmss;
-val with_thmss_i = gen_with_thmss have_thmss_i;
+val with_thmss = gen_with_thmss note_thmss;
+val with_thmss_i = gen_with_thmss note_thmss_i;
 
 end;
 
@@ -562,8 +561,8 @@
 
 in
 
-val using_thmss = gen_using_thmss ProofContext.have_thmss;
-val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
+val using_thmss = gen_using_thmss ProofContext.note_thmss;
+val using_thmss_i = gen_using_thmss ProofContext.note_thmss_i;
 
 end;
 
@@ -650,7 +649,7 @@
     |> map_context (ProofContext.qualified true)
     |> assume_i assumptions
     |> map_context (ProofContext.hide_thms false qnames)
-    |> (fn st => simple_have_thms name (the_facts st) st)
+    |> (fn st => simple_note_thms name (the_facts st) st)
     |> map_context (ProofContext.restore_qualified (context_of state))
   end;
 
@@ -811,7 +810,7 @@
     outer_state
     |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
     |> (fn st => Seq.map (fn res =>
-      have_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
+      note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
     |> (Seq.flat o Seq.map opt_solve)
     |> (Seq.flat o Seq.map after_qed)
   end;
@@ -855,10 +854,10 @@
             if name = "" andalso null loc_atts then thy'
             else (thy', ctxt')
               |> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
-      |> Locale.smart_have_thmss k locale_spec
+      |> Locale.smart_note_thmss k locale_spec
         ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
       |> (fn (thy, res) => (thy, res)
-          |>> (#1 o Locale.smart_have_thmss k locale_spec
+          |>> (#1 o Locale.smart_note_thmss k locale_spec
             [((name, atts), [(flat (map #2 res), [])])]));
   in (theory', ((k, name), results')) end;
 
diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -84,10 +84,10 @@
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
-  val have_thmss:
+  val note_thmss:
     ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
       context -> context * (bstring * thm list) list
-  val have_thmss_i:
+  val note_thmss_i:
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
       context -> context * (bstring * thm list) list
   val export_assume: exporter
@@ -1035,11 +1035,11 @@
       cases, defs));
 
 
-(* have_thmss *)
+(* note_thmss *)
 
 local
 
-fun gen_have_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
+fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
   let
     fun app ((ct, ths), (th, attrs)) =
       let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
@@ -1048,12 +1048,12 @@
     val thms = flat (rev rev_thms);
   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
 
-fun gen_have_thmss get args ctxt = foldl_map (gen_have_thss get) (ctxt, args);
+fun gen_note_thmss get args ctxt = foldl_map (gen_note_thss get) (ctxt, args);
 
 in
 
-val have_thmss = gen_have_thmss get_thms;
-val have_thmss_i = gen_have_thmss (K I);
+val note_thmss = gen_note_thmss get_thms;
+val note_thmss_i = gen_note_thmss (K I);
 
 end;
 
@@ -1119,7 +1119,7 @@
     val (ctxt', [(_, thms)]) =
       ctxt
       |> auto_bind_facts props
-      |> have_thmss_i [((name, attrs), ths)];
+      |> note_thmss_i [((name, attrs), ths)];
   in (ctxt', (cprops, (name, asms), (name, thms))) end;
 
 fun gen_assms prepp exp args ctxt =
diff -r 4bf2d10461f3 -r 3667b4616e9a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Apr 14 13:26:27 2004 +0200
+++ b/src/Pure/pure_thy.ML	Wed Apr 14 13:28:46 2004 +0200
@@ -42,9 +42,9 @@
   val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
   val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
     -> theory * thm list list
-  val have_thmss: theory attribute -> ((bstring * theory attribute list) *
+  val note_thmss: theory attribute -> ((bstring * theory attribute list) *
     (xstring * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
-  val have_thmss_i: theory attribute -> ((bstring * theory attribute list) *
+  val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
     (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
@@ -329,11 +329,11 @@
 val add_thms = gen_add_thms (name_thms true);
 
 
-(* have_thmss(_i) *)
+(* note_thmss(_i) *)
 
 local
 
-fun gen_have_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
+fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
   let
     fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
     val (thy', thms) = enter_thms (Theory.sign_of thy)
@@ -341,13 +341,13 @@
       (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
   in (thy', (bname, thms)) end;
 
-fun gen_have_thmss get kind_att args thy =
-  foldl_map (gen_have_thss get kind_att) (thy, args);
+fun gen_note_thmss get kind_att args thy =
+  foldl_map (gen_note_thss get kind_att) (thy, args);
 
 in
 
-val have_thmss = gen_have_thmss get_thms;
-val have_thmss_i = gen_have_thmss (K I);
+val note_thmss = gen_note_thmss get_thms;
+val note_thmss_i = gen_note_thmss (K I);
 
 end;