src/HOL/ex/ROOT.ML
changeset 33356 9157d0f9f00e
parent 32615 20f1edc87b7d
child 33436 0b5f07dd68f5
--- a/src/HOL/ex/ROOT.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Oct 30 13:59:49 2009 +0100
@@ -45,8 +45,6 @@
   "Groebner_Examples",
   "MT",
   "Unification",
-  "Commutative_RingEx",
-  "Commutative_Ring_Complete",
   "Primrec",
   "Tarski",
   "Adder",