src/Pure/Isar/proof.ML

   val refine_end: (context -> method) -> state -> state Seq.seq
   val match_bind: (string list * string) list -> state -> state
   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
   val with_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state

 val match_bind_i = gen_bind (ProofContext.match_bind_i false);
 val let_bind = gen_bind (ProofContext.match_bind true);
 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)
   |> these_factss;
 
 in
 
-val have_thmss = gen_have_thmss ProofContext.have_thmss;
-val have_thmss_i = gen_have_thmss ProofContext.have_thmss_i;
-
-fun simple_have_thms name thms = have_thmss_i [((name, []), [(thms, [])])];
+val note_thmss = gen_note_thmss ProofContext.note_thmss;
+val note_thmss_i = gen_note_thmss ProofContext.note_thmss_i;
+
+fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
 
 end;
 
 
 (* with_thmss *)
 
 local
 
 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;
 
 
 (* using_thmss *)

     let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
     in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), x)) end);
 
 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;
 
 
 (* locale instantiation *)

     state'
     |> add_binds_i lets
     |> 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;
 
 
 

     conditional pr (fn () => print_result goal_ctxt
       (kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
     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;
 
 fun local_qed finalize print state =

           |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results') ~~ loc_attss)
           |> (fn ((thy', ctxt'), res) =>
             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;
 
 
 (*note: clients should inspect first result only, as backtracking may destroy theory*)