89 -> Proof.context * (term list list * (Proof.context -> Proof.context)) |
89 -> Proof.context * (term list list * (Proof.context -> Proof.context)) |
90 val bind_propp_schematic_i: Proof.context * (term * term list) list list |
90 val bind_propp_schematic_i: Proof.context * (term * term list) list list |
91 -> Proof.context * (term list list * (Proof.context -> Proof.context)) |
91 -> Proof.context * (term list list * (Proof.context -> Proof.context)) |
92 val fact_tac: thm list -> int -> tactic |
92 val fact_tac: thm list -> int -> tactic |
93 val some_fact_tac: Proof.context -> int -> tactic |
93 val some_fact_tac: Proof.context -> int -> tactic |
94 val get_thm: Proof.context -> Facts.ref -> thm |
94 val get_fact: Proof.context -> Facts.ref -> thm list |
95 val get_thms: Proof.context -> Facts.ref -> thm list |
95 val get_fact_single: Proof.context -> Facts.ref -> thm |
|
96 val get_thms: Proof.context -> xstring -> thm list |
|
97 val get_thm: Proof.context -> xstring -> thm |
96 val valid_thms: Proof.context -> string * thm list -> bool |
98 val valid_thms: Proof.context -> string * thm list -> bool |
97 val add_path: string -> Proof.context -> Proof.context |
99 val add_path: string -> Proof.context -> Proof.context |
98 val no_base_names: Proof.context -> Proof.context |
100 val no_base_names: Proof.context -> Proof.context |
99 val qualified_names: Proof.context -> Proof.context |
101 val qualified_names: Proof.context -> Proof.context |
100 val sticky_prefix: string -> Proof.context -> Proof.context |
102 val sticky_prefix: string -> Proof.context -> Proof.context |
810 (case Facts.lookup local_facts name of |
812 (case Facts.lookup local_facts name of |
811 SOME ths => map (Thm.transfer thy) (Facts.select thmref ths) |
813 SOME ths => map (Thm.transfer thy) (Facts.select thmref ths) |
812 | NONE => from_thy thy xthmref); |
814 | NONE => from_thy thy xthmref); |
813 in pick name thms end; |
815 in pick name thms end; |
814 |
816 |
815 val get_thm = retrieve_thms PureThy.get_thms Facts.the_single; |
817 val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I); |
816 val get_thms = retrieve_thms PureThy.get_thms (K I); |
818 |
817 val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I); |
819 val get_fact = retrieve_thms PureThy.get_fact (K I); |
|
820 val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single; |
|
821 |
|
822 fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE)); |
|
823 fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE)); |
818 |
824 |
819 |
825 |
820 (* valid_thms *) |
826 (* valid_thms *) |
821 |
827 |
822 fun valid_thms ctxt (name, ths) = |
828 fun valid_thms ctxt (name, ths) = |
823 (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of |
829 (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of |
824 NONE => false |
830 NONE => false |
825 | SOME ths' => Thm.eq_thms (ths, ths')); |
831 | SOME ths' => Thm.eq_thms (ths, ths')); |
826 |
832 |
827 |
833 |
828 (* name space operations *) |
834 (* name space operations *) |
857 val Mode {stmt, ...} = get_mode ctxt; |
863 val Mode {stmt, ...} = get_mode ctxt; |
858 in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end); |
864 in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end); |
859 |
865 |
860 in |
866 in |
861 |
867 |
862 fun note_thmss k = gen_note_thmss get_thms k; |
868 fun note_thmss k = gen_note_thmss get_fact k; |
863 fun note_thmss_i k = gen_note_thmss (K I) k; |
869 fun note_thmss_i k = gen_note_thmss (K I) k; |
864 |
870 |
865 end; |
871 end; |
866 |
872 |
867 |
873 |