| Wed, 21 Jul 2010 16:49:52 +0200 | wenzelm | recovered benchmarks, which are not tested automatically; | changeset | files |
| Wed, 21 Jul 2010 16:29:20 +0200 | wenzelm | reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable; | changeset | files |
| Wed, 21 Jul 2010 16:14:16 +0200 | wenzelm | eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; | changeset | files |
| Wed, 21 Jul 2010 15:44:36 +0200 | wenzelm | moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; | changeset | files |
| Wed, 21 Jul 2010 15:31:38 +0200 | wenzelm | replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state; | changeset | files |
| Wed, 21 Jul 2010 15:23:46 +0200 | wenzelm | thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state; | changeset | files |
| Wed, 21 Jul 2010 15:13:36 +0200 | wenzelm | explicit dependency on theory HOL; | changeset | files |