equal
deleted
inserted
replaced
12 val generate_accessibility : |
12 val generate_accessibility : |
13 Proof.context -> theory list -> bool -> string -> unit |
13 Proof.context -> theory list -> bool -> string -> unit |
14 val generate_features : |
14 val generate_features : |
15 Proof.context -> string -> theory list -> string -> unit |
15 Proof.context -> string -> theory list -> string -> unit |
16 val generate_isar_dependencies : |
16 val generate_isar_dependencies : |
17 Proof.context -> theory list -> bool -> string -> unit |
17 Proof.context -> int * int option -> theory list -> bool -> string -> unit |
18 val generate_prover_dependencies : |
18 val generate_prover_dependencies : |
19 Proof.context -> params -> int * int option -> theory list -> bool -> string |
19 Proof.context -> params -> int * int option -> theory list -> bool -> string |
20 -> unit |
20 -> unit |
21 val generate_isar_commands : |
21 val generate_isar_commands : |
22 Proof.context -> string -> (int * int option) * int -> theory list -> bool |
22 Proof.context -> string -> (int * int option) * int -> theory list -> bool |
132 "" |
132 "" |
133 val lines = Par_List.map do_fact (tag_list 1 facts) |
133 val lines = Par_List.map do_fact (tag_list 1 facts) |
134 in File.write_list path lines end |
134 in File.write_list path lines end |
135 |
135 |
136 fun generate_isar_dependencies ctxt = |
136 fun generate_isar_dependencies ctxt = |
137 generate_isar_or_prover_dependencies ctxt NONE (1, NONE) |
137 generate_isar_or_prover_dependencies ctxt NONE |
138 |
138 |
139 fun generate_prover_dependencies ctxt params = |
139 fun generate_prover_dependencies ctxt params = |
140 generate_isar_or_prover_dependencies ctxt (SOME params) |
140 generate_isar_or_prover_dependencies ctxt (SOME params) |
141 |
141 |
142 fun is_bad_query ctxt ho_atp step j th isar_deps = |
142 fun is_bad_query ctxt ho_atp step j th isar_deps = |