235 f name more_atts (map (apfst single) th_atts); |
235 f name more_atts (map (apfst single) th_atts); |
236 |
236 |
237 fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); |
237 fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); |
238 |
238 |
239 |
239 |
240 fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs); |
240 fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss (("", []), th_srcs); |
241 fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss ((None, []), th_srcs); |
241 fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss (("", []), th_srcs); |
242 val have_theorems = #1 oo (global_have_thmss (PureThy.have_thmss o Some) o Comment.ignore); |
242 val have_theorems = #1 oo (global_have_thmss PureThy.have_thmss o Comment.ignore); |
243 val have_theorems_i = #1 oo (gen_have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore); |
243 val have_theorems_i = #1 oo (gen_have_thmss_i PureThy.have_thmss o Comment.ignore); |
244 val have_lemmas = #1 oo (global_have_thmss (have_lemss o Some) o Comment.ignore); |
244 val have_lemmas = #1 oo (global_have_thmss have_lemss o Comment.ignore); |
245 val have_lemmas_i = #1 oo (gen_have_thmss_i (have_lemss o Some) o Comment.ignore); |
245 val have_lemmas_i = #1 oo (gen_have_thmss_i have_lemss o Comment.ignore); |
246 val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore; |
246 val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore; |
247 val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore; |
247 val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore; |
248 |
248 |
249 |
249 |
250 (* forward chaining *) |
250 (* forward chaining *) |