# HG changeset patch
# User chaieb
# Date 1233321863 0
# Node ID e8785144719d56f775a4aafd2c43e97ec7157f64
# Parent  477c7fcc0777ec94a5a392f07f1cd70c9a4d98e0
Added Formal_Power_Series_Examples to HOL-ex image

diff -r 477c7fcc0777 -r e8785144719d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 30 13:24:23 2009 +0000
+++ b/src/HOL/IsaMakefile	Fri Jan 30 13:24:23 2009 +0000
@@ -800,7 +800,7 @@
   ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
   ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
   ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
-  ex/CodegenSML_Test.thy 						\
+  ex/CodegenSML_Test.thy ex/Formal_power_Series_Examples.thy						\
   ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
   ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy		\
   ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy	\
diff -r 477c7fcc0777 -r e8785144719d src/HOL/ex/ROOT.ML
--- 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";