equal
deleted
inserted
replaced
14 |
14 |
15 (*.get all theorems used by isac and defined in isabelle.*) |
15 (*.get all theorems used by isac and defined in isabelle.*) |
16 local |
16 local |
17 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
17 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
18 (map (thms_of_rls o #2 o #2))) (!ruleset'); |
18 (map (thms_of_rls o #2 o #2))) (!ruleset'); |
19 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory'); |
19 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) |
|
20 (*WN100827 TODOOOOO*)(!theory'); |
20 in |
21 in |
21 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
22 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
22 end; |
23 end; |
23 |
24 |
24 (*.set up the list using 'val first_isac_thy' (see ListC.ML).*) |
25 (*.set up the list using 'val first_isac_thy' (see ListC.ML).*) |
29 (*.create the hierarchy of theory elements from IsacKnowledge |
30 (*.create the hierarchy of theory elements from IsacKnowledge |
30 including thms from Isabelle used in rls; |
31 including thms from Isabelle used in rls; |
31 elements store_*d in any *.ML are not overwritten.*) |
32 elements store_*d in any *.ML are not overwritten.*) |
32 |
33 |
33 thehier := the_hier (!thehier) (collect_thydata ()); |
34 thehier := the_hier (!thehier) (collect_thydata ()); |
34 writeln("----------------------------------\n\ |
35 writeln("----------------------------------\n" ^ |
35 \*** insert: not found ... IS OK : \n\ |
36 "*** insert: not found ... IS OK : \n" ^ |
36 \comes from fill_parents \n\ |
37 "comes from fill_parents \n" ^ |
37 \----------------------------------\n"); |
38 "----------------------------------\n"); |