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";