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