Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 Sep 2010 12:56:51 +0200] rev 38013
interrupted update test/../Knowledge/integrate.sml, repaired term2str
term2str by help from Florian and Jasmin; took the former.
Found at that point in integrate.sml,
that all "op +" etc need to be updated.
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 Sep 2010 08:54:26 +0200] rev 38012
tuned pbt's due to copy_named
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 Sep 2010 08:43:36 +0200] rev 38011
repaired is_copy_named, cpy_nam and improved tests & comments
Walther Neuper <neuper@ist.tugraz.at> [Tue, 14 Sep 2010 15:46:56 +0200] rev 38010
repaired copy_nam
Walther Neuper <neuper@ist.tugraz.at> [Tue, 14 Sep 2010 12:12:42 +0200] rev 38009
adapted is_copy_named from v___ to v'''
Unclear comment for 'fun is_copy_named_generating',
thus probably still broken; waiting for further tests.
Tests are still run from Build_Isac.
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