equal
deleted
inserted
replaced
100 |> map snd |
100 |> map snd |
101 val all_names = all_names ths |
101 val all_names = all_names ths |
102 fun do_thm th = |
102 fun do_thm th = |
103 let |
103 let |
104 val name = nickname_of th |
104 val name = nickname_of th |
105 val deps = isar_dependencies_of all_names th |
105 val deps = isar_dependencies_of all_names th |> these |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
107 in File.append path s end |
107 in File.append path s end |
108 in List.app do_thm ths end |
108 in List.app do_thm ths end |
109 |
109 |
110 fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy |
110 fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy |
120 val all_names = all_names ths |
120 val all_names = all_names ths |
121 fun do_thm th = |
121 fun do_thm th = |
122 let |
122 let |
123 val name = nickname_of th |
123 val name = nickname_of th |
124 val deps = |
124 val deps = |
125 atp_dependencies_of ctxt params prover false facts all_names th |
125 case atp_dependencies_of ctxt params prover 0 facts all_names th of |
|
126 SOME deps => deps |
|
127 | NONE => isar_dependencies_of all_names th |> these |
126 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
128 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
127 in File.append path s end |
129 in File.append path s end |
128 in List.app do_thm ths end |
130 in List.app do_thm ths end |
129 |
131 |
130 fun generate_commands ctxt prover thy file_name = |
132 fun generate_commands ctxt prover thy file_name = |
140 val all_names = all_names ths |
142 val all_names = all_names ths |
141 fun do_fact ((_, stature), th) prevs = |
143 fun do_fact ((_, stature), th) prevs = |
142 let |
144 let |
143 val name = nickname_of th |
145 val name = nickname_of th |
144 val feats = features_of ctxt prover thy stature [prop_of th] |
146 val feats = features_of ctxt prover thy stature [prop_of th] |
145 val deps = isar_dependencies_of all_names th |
147 val deps = isar_dependencies_of all_names th |> these |
146 val kind = Thm.legacy_get_kind th |
148 val kind = Thm.legacy_get_kind th |
147 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
149 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
148 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
150 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
149 val update = |
151 val update = |
150 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
152 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |