equal
deleted
inserted
replaced
15 val generate_isar_dependencies : |
15 val generate_isar_dependencies : |
16 theory -> bool -> string -> unit |
16 theory -> bool -> string -> unit |
17 val generate_atp_dependencies : |
17 val generate_atp_dependencies : |
18 Proof.context -> params -> theory -> bool -> string -> unit |
18 Proof.context -> params -> theory -> bool -> string -> unit |
19 val generate_commands : Proof.context -> string -> theory -> string -> unit |
19 val generate_commands : Proof.context -> string -> theory -> string -> unit |
20 val generate_iter_suggestions : |
20 val generate_mepo_suggestions : |
21 Proof.context -> params -> theory -> int -> string -> unit |
21 Proof.context -> params -> theory -> int -> string -> unit |
22 end; |
22 end; |
23 |
23 |
24 structure MaSh_Export : MASH_EXPORT = |
24 structure MaSh_Export : MASH_EXPORT = |
25 struct |
25 struct |
180 in [name] end |
180 in [name] end |
181 val thy_map = old_facts |> thy_map_from_facts |
181 val thy_map = old_facts |> thy_map_from_facts |
182 val parents = parent_facts thy thy_map |
182 val parents = parent_facts thy thy_map |
183 in fold do_fact new_facts parents; () end |
183 in fold do_fact new_facts parents; () end |
184 |
184 |
185 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
185 fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant |
186 file_name = |
186 file_name = |
187 let |
187 let |
188 val path = file_name |> Path.explode |
188 val path = file_name |> Path.explode |
189 val _ = File.write path "" |
189 val _ = File.write path "" |
190 val prover = hd provers |
190 val prover = hd provers |