equal
deleted
inserted
replaced
70 val smart_store_thms_open: (bstring * thm list) -> thm list |
70 val smart_store_thms_open: (bstring * thm list) -> thm list |
71 val forall_elim_var: int -> thm -> thm |
71 val forall_elim_var: int -> thm -> thm |
72 val forall_elim_vars: int -> thm -> thm |
72 val forall_elim_vars: int -> thm -> thm |
73 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
73 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
74 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
74 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
|
75 val note: string -> string * thm -> theory -> thm * theory |
75 val note_thmss: string -> ((bstring * attribute list) * |
76 val note_thmss: string -> ((bstring * attribute list) * |
76 (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
77 (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
77 val note_thmss_i: string -> ((bstring * attribute list) * |
78 val note_thmss_i: string -> ((bstring * attribute list) * |
78 (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
79 (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
79 val note_thmss_qualified: string -> string -> ((bstring * attribute list) * |
80 val note_thmss_qualified: string -> string -> ((bstring * attribute list) * |
395 |
396 |
396 val note_thmss = gen_note_thmss get_thms; |
397 val note_thmss = gen_note_thmss get_thms; |
397 val note_thmss_i = gen_note_thmss (K I); |
398 val note_thmss_i = gen_note_thmss (K I); |
398 |
399 |
399 end; |
400 end; |
|
401 |
|
402 fun note kind (name, thm) = |
|
403 note_thmss_i kind [((name, []), [([thm], [])])] |
|
404 #>> (fn [(_, [thm])] => thm); |
400 |
405 |
401 fun note_thmss_qualified k path facts thy = |
406 fun note_thmss_qualified k path facts thy = |
402 thy |
407 thy |
403 |> Sign.add_path path |
408 |> Sign.add_path path |
404 |> Sign.no_base_names |
409 |> Sign.no_base_names |