107 val custom_accesses: (string list -> string list list) -> context -> context |
107 val custom_accesses: (string list -> string list list) -> context -> context |
108 val restore_naming: context -> context -> context |
108 val restore_naming: context -> context -> context |
109 val hide_thms: bool -> string list -> context -> context |
109 val hide_thms: bool -> string list -> context -> context |
110 val put_thms: string * thm list option -> context -> context |
110 val put_thms: string * thm list option -> context -> context |
111 val note_thmss: |
111 val note_thmss: |
112 ((bstring * context attribute list) * (thmref * context attribute list) list) list -> |
112 ((bstring * attribute list) * (thmref * attribute list) list) list -> |
113 context -> (bstring * thm list) list * context |
113 context -> (bstring * thm list) list * context |
114 val note_thmss_i: |
114 val note_thmss_i: |
115 ((bstring * context attribute list) * (thm list * context attribute list) list) list -> |
115 ((bstring * attribute list) * (thm list * attribute list) list) list -> |
116 context -> (bstring * thm list) list * context |
116 context -> (bstring * thm list) list * context |
117 val read_vars: (string * string option * mixfix) list -> context -> |
117 val read_vars: (string * string option * mixfix) list -> context -> |
118 (string * typ option * mixfix) list * context |
118 (string * typ option * mixfix) list * context |
119 val cert_vars: (string * typ option * mixfix) list -> context -> |
119 val cert_vars: (string * typ option * mixfix) list -> context -> |
120 (string * typ option * mixfix) list * context |
120 (string * typ option * mixfix) list * context |
127 val add_fixes_legacy: (string * typ option * mixfix) list -> context -> string list * context |
127 val add_fixes_legacy: (string * typ option * mixfix) list -> context -> string list * context |
128 val fix_frees: term -> context -> context |
128 val fix_frees: term -> context -> context |
129 val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) |
129 val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) |
130 val bind_fixes: string list -> context -> (term -> term) * context |
130 val bind_fixes: string list -> context -> (term -> term) * context |
131 val add_assms: export -> |
131 val add_assms: export -> |
132 ((string * context attribute list) * (string * (string list * string list)) list) list -> |
132 ((string * attribute list) * (string * (string list * string list)) list) list -> |
133 context -> (bstring * thm list) list * context |
133 context -> (bstring * thm list) list * context |
134 val add_assms_i: export -> |
134 val add_assms_i: export -> |
135 ((string * context attribute list) * (term * (term list * term list)) list) list -> |
135 ((string * attribute list) * (term * (term list * term list)) list) list -> |
136 context -> (bstring * thm list) list * context |
136 context -> (bstring * thm list) list * context |
137 val assume_export: export |
137 val assume_export: export |
138 val presume_export: export |
138 val presume_export: export |
139 val add_view: context -> cterm list -> context -> context |
139 val add_view: context -> cterm list -> context -> context |
140 val export_view: cterm list -> context -> context -> thm -> thm |
140 val export_view: cterm list -> context -> context -> thm -> thm |
1040 local |
1040 local |
1041 |
1041 |
1042 fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt => |
1042 fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt => |
1043 let |
1043 let |
1044 fun app (th, attrs) (ct, ths) = |
1044 fun app (th, attrs) (ct, ths) = |
1045 let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th) |
1045 let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th) |
1046 in (ct', th' :: ths) end; |
1046 in (ct', th' :: ths) end; |
1047 val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []); |
1047 val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []); |
1048 val thms = List.concat (rev rev_thms); |
1048 val thms = List.concat (rev rev_thms); |
1049 in ((name, thms), ctxt' |> put_thms (name, SOME thms)) end); |
1049 in ((name, thms), ctxt' |> put_thms (name, SOME thms)) end); |
1050 |
1050 |