author wenzelm Sat, 08 Jul 2006 12:54:40 +0200 changeset 20052 3d4ff822d0b3 parent 20051 859e7129961b child 20053 7f32ce6354d6
presburger_ss: proper context; Goal.prove: context;
```--- a/src/HOL/Integ/cooper_proof.ML	Sat Jul 08 12:54:39 2006 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Sat Jul 08 12:54:40 2006 +0200
@@ -30,13 +30,9 @@
struct
open CooperDec;

-(*
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
-*)
+val presburger_ss = simpset ()
+  addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];

-val presburger_ss = simpset_of (theory "Presburger")
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;

(*Theorems that will be used later for the proofgeneration*)
@@ -44,7 +40,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";

-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)

val ac_lt_eq =  thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -194,7 +190,7 @@
(essentially) that are only to make at runtime.*)
(* ------------------------------------------------------------------------- *)
fun prove_elementar thy s fm2 =
-  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
+  Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
(case s of
(*"ss" like simplification with simpset*)
"ss" =>```
```--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jul 08 12:54:39 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jul 08 12:54:40 2006 +0200
@@ -30,13 +30,9 @@
struct
open CooperDec;

-(*
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
-*)
+val presburger_ss = simpset ()
+  addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];

-val presburger_ss = simpset_of (theory "Presburger")
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;

(*Theorems that will be used later for the proofgeneration*)
@@ -44,7 +40,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";

-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)

val ac_lt_eq =  thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -194,7 +190,7 @@
(essentially) that are only to make at runtime.*)
(* ------------------------------------------------------------------------- *)
fun prove_elementar thy s fm2 =
-  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
+  Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
(case s of
(*"ss" like simplification with simpset*)
"ss" =>```