# HG changeset patch
# User huffman
# Date 1323847968 -3600
# Node ID 9ae1c60db357238d55b0fd4674635181238d6021
# Parent  c7a73fb9be68d62e9c9bfedd19bf9c8638739a52
replace 'lemmas' with 'lemma'

diff -r c7a73fb9be68 -r 9ae1c60db357 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 14 07:38:30 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 14 08:32:48 2011 +0100
@@ -2601,7 +2601,8 @@
 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
   unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
 
-lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
+lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)"
+  by (simp only: word_number_of_def shiftl1_def)
 
 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
   by (rule trans [OF _ shiftl1_number]) simp