equal
deleted
inserted
replaced
31 val ths = facts |> map snd |
31 val ths = facts |> map snd |
32 val all_names = ths |> map Thm.get_name_hint |
32 val all_names = ths |> map Thm.get_name_hint |
33 fun do_fact ((_, (_, status)), th) prevs = |
33 fun do_fact ((_, (_, status)), th) prevs = |
34 let |
34 let |
35 val name = Thm.get_name_hint th |
35 val name = Thm.get_name_hint th |
36 val feats = features_of thy (status, th) |
36 val feats = features_of thy status [prop_of 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 space_implode " " prevs ^ "; " ^ space_implode " " feats |
41 space_implode " " prevs ^ "; " ^ space_implode " " feats |