Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 Sep 2010 18:37:16 +0200] rev 38008
tuned
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 Sep 2010 18:12:15 +0200] rev 38007
ref --> Unsynchronized.ref tuned.
there are differences in compiling via (1) Build_Isac.thy and via (2) ROOT.ML:
# (1) still accepts ref, while (2) requires Unsynchronized.ref
# (2) is more rigid in type checking (eg. "can't find a fixed record type")
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 Sep 2010 17:21:22 +0200] rev 38006
ref --> Unsynchronized.ref done
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 Sep 2010 16:36:14 +0200] rev 38005
tuned, before changing ref --> Unsynchronized.ref
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 Sep 2010 15:42:03 +0200] rev 38004
added src/Tools/isac/ROOT.ML
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 Sep 2010 12:15:18 +0200] rev 38003
----- 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"
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 Sep 2010 11:58:46 +0200] rev 38002
intermediate in Knowledge/Isac.thy
adapted all code to Theory.axioms_of, which returns terms instead of thms
Isac.thy not finished
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 Sep 2010 10:36:41 +0200] rev 38001
updated Knowledge/Test.thy
Walther Neuper <neuper@ist.tugraz.at> [Thu, 09 Sep 2010 13:39:30 +0200] rev 38000
updated Knowledge/AlgEin.thy
Walther Neuper <neuper@ist.tugraz.at> [Thu, 09 Sep 2010 13:31:36 +0200] rev 37999
updated Knowledge/Biegelinie.thy