40 print_depth 99; map string_of_thy ancestors; print_depth 3; |
40 print_depth 99; map string_of_thy ancestors; print_depth 3; |
41 length ancestors; |
41 length ancestors; |
42 val ancestors = (#ancestors o rep_theory) first_isac_thy; |
42 val ancestors = (#ancestors o rep_theory) first_isac_thy; |
43 length ancestors; |
43 length ancestors; |
44 print_depth 99; map theory2theory' ancestors; print_depth 3; |
44 print_depth 99; map theory2theory' ancestors; print_depth 3; |
45 val isabthms = (flat o (map thms_of)) ancestors; |
45 val isabthms = (flat o (map PureThy.all_thms_of)) ancestors; |
46 length isabthms; |
46 length isabthms; |
47 |
47 |
48 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset'); |
48 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset'); |
49 (*thms from rulesets*) |
49 (*thms from rulesets*) |
50 val isacrlsthms = ((map rep_thm_G') o flat o |
50 val isacrlsthms = ((map rep_thm_G') o flat o |
51 (map (thms_of_rls o #2 o #2))) (!ruleset'); |
51 (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset'); |
52 length isacrlsthms; |
52 length isacrlsthms; |
53 (*takes a few seconds... |
53 (*takes a few seconds... |
54 val isacrlsthms = gen_distinct eq_thmI isacrlsthms; |
54 val isacrlsthms = gen_distinct eq_thmI isacrlsthms; |
55 length isacrlsthms; |
55 length isacrlsthms; |
56 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv"; |
56 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv"; |
58 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^"; |
58 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^"; |
59 ...*) |
59 ...*) |
60 |
60 |
61 (!theory'); |
61 (!theory'); |
62 map #2 (!theory'); |
62 map #2 (!theory'); |
63 map (thms_of o #2) (!theory'); |
63 map (PureThy.all_thms_of o #2) (!theory'); |
64 val isacthms = (flat o (map (thms_of o #2))) (!theory'); |
64 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory'); |
65 (*takes a few seconds... |
65 (*takes a few seconds... |
66 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
66 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
67 length rlsthmsNOTisac; |
67 length rlsthmsNOTisac; |
68 "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv"; |
68 "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv"; |
69 print_depth 99; map #1 rlsthmsNOTisac; print_depth 3; |
69 print_depth 99; map #1 rlsthmsNOTisac; print_depth 3; |
70 "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^"; |
70 "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^"; |
71 ...*) |
71 ...*) |
72 |
72 |
73 "----- for 'fun make_isab_thm_thy'"; |
73 "----- for 'fun make_isab_thm_thy'"; |
74 gen_inter eq_thmI (isacrlsthms, (thms_of (nth 1 ancestors))); |
74 inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors)); |
75 gen_inter eq_thmI; |
75 inter eq_thmI; |
76 curry (gen_inter eq_thmI); |
76 (inter eq_thmI); |
77 curry (gen_inter eq_thmI) isacrlsthms; |
77 (inter eq_thmI) isacrlsthms; |
78 (*takes a few seconds... |
78 (*takes a few seconds... |
79 curry (gen_inter eq_thmI) isacrlsthms (thms_of (nth 9 ancestors)); |
79 curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors)); |
80 |
80 |
81 val thy = (nth 52 ancestors); |
81 val thy = (nth 52 ancestors); |
82 val sec = (curry (gen_inter eq_thmI) isacrlsthms o thms_of) (nth 52 ancestors); |
82 val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors); |
83 length (thms_of (nth 9 ancestors)); |
83 length (PureThy.all_thms_of (nth 9 ancestors)); |
84 length sec; |
84 length sec; |
85 ...*) |
85 ...*) |
86 |
86 |
87 (*takes 1 minute... |
87 (*takes 1 minute... |
88 print_depth 99; |
88 print_depth 99; |
89 map (curry (gen_inter eq_thmI) rlsthmsNOTisac o thms_of) ancestors; |
89 map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors; |
90 print_depth 3; |
90 print_depth 3; |
91 *) |
91 *) |
92 |
92 |
93 (*takes some seconds... |
93 (*takes some seconds... |
94 val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac))) |
94 val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac))) |