Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
presburger_ss: proper context;
authorwenzelm
Sat, 08 Jul 2006 12:54:40 +0200
changeset 20052 3d4ff822d0b3
parent 20051 859e7129961b
child 20053 7f32ce6354d6
presburger_ss: proper context; Goal.prove: context;
src/HOL/Integ/cooper_proof.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/cooper_proof.ML file | annotate | diff | comparison | revisions 
--- 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")
-  addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
 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")
-  addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
 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" =>
isabelle