Added Formal_Power_Series_Examples to HOL-ex image
authorchaieb
Fri Jan 30 13:24:23 2009 +0000 (2009-01-30)
changeset 29697e8785144719d
parent 29696 477c7fcc0777
child 29698 91feea8e41e4
Added Formal_Power_Series_Examples to HOL-ex image
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 30 13:24:23 2009 +0000
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 30 13:24:23 2009 +0000
     1.3 @@ -800,7 +800,7 @@
     1.4    ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
     1.5    ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
     1.6    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
     1.7 -  ex/CodegenSML_Test.thy 						\
     1.8 +  ex/CodegenSML_Test.thy ex/Formal_power_Series_Examples.thy						\
     1.9    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
    1.10    ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy		\
    1.11    ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy	\
     2.1 --- a/src/HOL/ex/ROOT.ML	Fri Jan 30 13:24:23 2009 +0000
     2.2 +++ b/src/HOL/ex/ROOT.ML	Fri Jan 30 13:24:23 2009 +0000
     2.3 @@ -73,7 +73,8 @@
     2.4    "MIR",
     2.5    "ReflectedFerrack",
     2.6    "Refute_Examples",
     2.7 -  "Quickcheck_Examples"
     2.8 +  "Quickcheck_Examples",
     2.9 +  "Formal_Power_Series_Examples"
    2.10  ];
    2.11  
    2.12  setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";