equal
deleted
inserted
replaced
1 (* export theory-data "thehier" to xml |
1 (* title: "xmlsrc/thy-hierarchy.sml" |
|
2 export theory-data "thehier" to xml |
2 author: Walther Neuper 0601 |
3 author: Walther Neuper 0601 |
3 (c) isac-team |
4 (c) isac-team |
4 *) |
5 *) |
5 |
6 |
6 open TermC (* allows contains_one_of to be infix *) |
7 open TermC (* allows contains_one_of to be infix *) |
9 fun thms_of thy = (* das ist zu verbessern *) |
10 fun thms_of thy = (* das ist zu verbessern *) |
10 let |
11 let |
11 val fun_ids = Specify.get_fun_ids thy |
12 val fun_ids = Specify.get_fun_ids thy |
12 in |
13 in |
13 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy |
14 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy |
14 andalso not (thm contains_one_of fun_ids)) |
15 andalso not (thm contains_one_of fun_ids) |
|
16 andalso not (Celem.thmID_of_derivation_name' thm = "mono")) |
|
17 (* created in Biegelinie by partial_function ^^^^^^*) |
15 (map snd (Global_Theory.all_thms_of thy false)) |
18 (map snd (Global_Theory.all_thms_of thy false)) |
16 end |
19 end |
17 |
20 |
18 (* wrap theory-data into the uniform type thydata *) |
21 (* wrap theory-data into the uniform type thydata *) |
19 |
22 |