Tue, 03 Aug 2010 18:13:57 +0200 | wenzelm | eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order; | changeset | files |
Tue, 03 Aug 2010 18:10:18 +0200 | wenzelm | find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145); | changeset | files |
Tue, 03 Aug 2010 16:57:45 +0200 | wenzelm | renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); | changeset | files |