# HG changeset patch
# User nipkow
# Date 1169740677 -3600
# Node ID a2c4861363d5d453d120b0cfc03130e0d36ab596
# Parent  5203eb387a0cae289ca00686bc807e764d182360
Allows evaluation of min/max o numerals.

diff -r 5203eb387a0c -r a2c4861363d5 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Thu Jan 25 09:32:56 2007 +0100
+++ b/src/HOL/Integ/Numeral.thy	Thu Jan 25 16:57:57 2007 +0100
@@ -74,6 +74,11 @@
   pred :: "int \<Rightarrow> int" where
   "pred k = k - 1"
 
+declare
+ max_def[of "number_of u" "number_of v", standard, simp]
+ min_def[of "number_of u" "number_of v", standard, simp]
+  -- {* unfolding @{text minx} and @{text max} on numerals *}
+
 lemmas numeral_simps = 
   succ_def pred_def Pls_def Min_def Bit_def