Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/nat_numeral_simprocs.ML
changeset 35092 cfe605c54e50
parent 35064 1bdef0c013d3
child 35267 8dfd816713c6 
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 14:12:04 2010 +0100
@@ -176,8 +176,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   val bal_add1 = @{thm nat_less_add_iff1} RS trans
   val bal_add2 = @{thm nat_less_add_iff2} RS trans
 );
@@ -185,8 +185,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   val bal_add1 = @{thm nat_le_add_iff1} RS trans
   val bal_add2 = @{thm nat_le_add_iff2} RS trans
 );
@@ -308,8 +308,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   val cancel = @{thm nat_mult_less_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -317,8 +317,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   val cancel = @{thm nat_mult_le_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -387,16 +387,16 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
 );
isabelle