intermed. repair thehier, the hierarchy of thy/thm for access by isac.
Problem with Theory.thms_of dropped from 2002 to 2009.
Now used Theory.axioms_of returning terms, which will cause problems,
when isac's Knowledge will prove axioms to thms.
intermed.: PureThy.all_thms_of cannot replace Theory.thms_of,
but Thm.derivation_name contains all data required ...TODO.
1 (* Title: trials on library.ML
2 Author: Walther Neuper, TU Graz, 101027
5 "--------------------------------------------------------";
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- fun foldl_map ------------------------------";
10 "--------------------------------------------------------";
11 "--------------------------------------------------------";
14 "----------- fun foldl_map ------------------------------";
15 "----------- fun foldl_map ------------------------------";
16 "----------- fun foldl_map ------------------------------";
17 fun arg1 (a, b) = (a, b + 10);
18 val arg2 = [("a1", 1), ("a2", 2), ("a3", 3)];
19 (*========== inhibit exn =======================================================
20 foldl_map arg1 arg2; (*why is this not known here, but the others below ?*)
21 ============ inhibit exn =====================================================*)