1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Thu Jun 28 19:09:36 2007 +0200
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Jun 28 19:09:38 2007 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Reflected_Presburger
     1.5 -imports GCD Main EfficientNat
     1.6 +imports GCD EfficientNat
     1.7  uses ("coopereif.ML") ("coopertac.ML")
     1.8  begin
     1.9  
    1.10 @@ -1902,18 +1902,21 @@
    1.11  
    1.12  theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
    1.13    using qelim_ci cooper prep by (auto simp add: pa_def)
    1.14 -declare zdvd_iff_zmod_eq_0 [code]
    1.15  
    1.16 -code_module GeneratedCooper
    1.17 -file "generated_cooper.ML"
    1.18 -contains pa = "pa"
    1.19 -test = "%x . pa (E(A(Imp (Ge (Sub (Bound 0) (Bound 1))) (E(E(Eq(Sub(Add(Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
    1.20 +definition
    1.21 +  cooper_test :: "unit \<Rightarrow> fm"
    1.22 +where
    1.23 +  "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
    1.24 +    (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
    1.25 +      (Bound 2))))))))"
    1.26  
    1.27 -ML{* use "generated_cooper.ML"; 
    1.28 -     GeneratedCooper.test (); *}
    1.29 +code_gen pa cooper_test in SML
    1.30 +
    1.31 +ML {* structure GeneratedCooper = struct open ROOT end *}
    1.32 +ML {* GeneratedCooper.Reflected_Presburger.cooper_test () *}
    1.33  use "coopereif.ML"
    1.34  oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
    1.35 -use"coopertac.ML"
    1.36 +use "coopertac.ML"
    1.37  setup "LinZTac.setup"
    1.38  
    1.39    (* Tests *)