--- 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;
--- 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);
--- 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'))))
--- 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;
--- 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 =
--- 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;