src/Tools/isac/xmlsrc/thy-hierarchy.sml
changeset 59549 e0e3d41ef86c
parent 59507 0c839aea0c2e
     1.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu May 30 12:39:13 2019 +0200
     1.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Sat Jun 01 11:09:19 2019 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -(* export theory-data "thehier" to xml
     1.5 +(* title: "xmlsrc/thy-hierarchy.sml"
     1.6 +     export theory-data "thehier" to xml
     1.7     author: Walther Neuper 0601
     1.8     (c) isac-team
     1.9  *)
    1.10 @@ -11,7 +12,9 @@
    1.11      val fun_ids = Specify.get_fun_ids thy
    1.12    in
    1.13      filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
    1.14 -        andalso not (thm contains_one_of fun_ids))
    1.15 +        andalso not (thm contains_one_of fun_ids)
    1.16 +        andalso not (Celem.thmID_of_derivation_name' thm = "mono"))
    1.17 +        (* created in Biegelinie by partial_function ^^^^^^*)
    1.18        (map snd (Global_Theory.all_thms_of thy false))
    1.19    end
    1.20