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:41 +0200
changeset 20053 7f32ce6354d6
parent 20052 3d4ff822d0b3
child 20054 24d176b8f240
presburger_ss: proper context;
src/HOL/Integ/presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/presburger.ML	Sat Jul 08 12:54:40 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Sat Jul 08 12:54:41 2006 +0200
@@ -30,7 +30,7 @@
 (*-----------------------------------------------------------------*)
 
 
-val presburger_ss = simpset_of (theory "Presburger");
+val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
--- a/src/HOL/Tools/Presburger/presburger.ML	Sat Jul 08 12:54:40 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jul 08 12:54:41 2006 +0200
@@ -30,7 +30,7 @@
 (*-----------------------------------------------------------------*)
 
 
-val presburger_ss = simpset_of (theory "Presburger");
+val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
isabelle