src/HOL/ex/ROOT.ML
changeset 29697 e8785144719d
parent 29650 cc3958d31b1d
child 29704 9a7d84fd83c6
--- a/src/HOL/ex/ROOT.ML	Fri Jan 30 13:24:23 2009 +0000
+++ b/src/HOL/ex/ROOT.ML	Fri Jan 30 13:24:23 2009 +0000
@@ -73,7 +73,8 @@
   "MIR",
   "ReflectedFerrack",
   "Refute_Examples",
-  "Quickcheck_Examples"
+  "Quickcheck_Examples",
+  "Formal_Power_Series_Examples"
 ];
 
 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";