equal
deleted
inserted
replaced
36 val feats = features_of thy (status, th) |
36 val feats = features_of thy (status, th) |
37 val deps = isabelle_dependencies_of all_names th |
37 val deps = isabelle_dependencies_of all_names th |
38 val kind = Thm.legacy_get_kind th |
38 val kind = Thm.legacy_get_kind th |
39 val name = fact_name_of name |
39 val name = fact_name_of name |
40 val core = |
40 val core = |
41 name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats |
41 space_implode " " prevs ^ "; " ^ space_implode " " feats |
42 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
42 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
43 val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n" |
43 val update = |
|
44 "! " ^ name ^ ": " ^ core ^ "; " ^ space_implode " " deps ^ "\n" |
44 val _ = File.append path (query ^ update) |
45 val _ = File.append path (query ^ update) |
45 in [name] end |
46 in [name] end |
46 val thy_ths = old_facts |> thms_by_thy |
47 val thy_ths = old_facts |> thms_by_thy |
47 val parents = parent_facts thy_ths thy |
48 val parents = parent_facts thy_ths thy |
48 in fold do_fact new_facts parents; () end |
49 in fold do_fact new_facts parents; () end |