----- update of isac SYNTAX Isabelle2002 --> Isabelle2009-2 finished.
Semantic check is to be done. Known problems (see #974b):
# hierarchy of theory elements for IsacKnowledge seems empty
(no ouput befor *** insert: not found ... IS OK)
# copynamed ___ --> ''' in Interpreter
# Subproblem (Thy', ... instead of Thy_ in Interpreter
# theory' handled inconsistently: "Thy" | "Thy.thy"
# thm' handled inconsistently: "refl" | "Test.refl" | "Test.class.refl"
1.1 --- a/src/Tools/isac/Knowledge/Isac.thy Fri Sep 10 11:58:46 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Fri Sep 10 12:15:18 2010 +0200
1.3 @@ -25,37 +25,19 @@
1.4 val allthys = Theory.ancestors_of @{theory}; (*116*)
1.5 val isabthys = Theory.ancestors_of first_isac_thy; (* 86; isa02:58*)
1.6 val isacthys = subtract Theory.eq_thy isabthys allthys; (* 30*)
1.7 -*}
1.8 -ML {*
1.9 +
1.10 val isacrlsthms = ((map (apsnd prop_of)) o
1.11 (gen_distinct eq_thmI) o (map rep_thm_G') o flat o
1.12 (map (thms_of_rls o #2 o #2))) (!ruleset');
1.13 -*}
1.14 -ML {*
1.15 val isacthms =
1.16 (flat o (map Theory.axioms_of)) isacthys : (thmID * term) list;
1.17 -
1.18 -*}
1.19 -
1.20 -ML {*
1.21 (*in*)
1.22 - val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
1.23 + val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
1.24 + (*length rlsthmsNOTisac;-->45*)
1.25 (*end;*)
1.26 -*}
1.27 -
1.28 -ML {*
1.29 -make_isab;
1.30 -collect_thydata;
1.31 -term2xml;
1.32 -*}
1.33 -ML {*
1.34
1.35 (*.set up the list using 'val first_isac_thy' (see ListC.ML).*)
1.36 isab_thm_thy := make_isab rlsthmsNOTisac isabthys;
1.37 -*}
1.38 -
1.39 -ML {*
1.40 -
1.41
1.42 (*.create the hierarchy of theory elements from IsacKnowledge
1.43 including thms from Isabelle used in rls;