author | wenzelm |
Thu, 20 Dec 2007 22:21:30 +0100 | |
changeset 25738 | b091cbae3e2a |
parent 25737 | 84c92fc48e36 |
child 25739 | 9da2343deb92 |
--- a/src/HOL/ex/ROOT.ML Thu Dec 20 21:14:28 2007 +0100 +++ b/src/HOL/ex/ROOT.ML Thu Dec 20 22:21:30 2007 +0100 @@ -53,15 +53,14 @@ "Random", "Primrec", "Tarski", - "Adder" + "Adder", + "Classical", + "set", + "Meson_Test" ]; setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical"; -time_use_thy "Classical"; -time_use_thy "set"; - -time_use_thy "Meson_Test"; time_use_thy "Dense_Linear_Order_Ex"; time_use_thy "PresburgerEx"; time_use_thy "Reflected_Presburger";