src/HOL/Word/Word.thy
changeset 61169 4de9ff3ea29a
parent 61076 bdc1e2f0a86a
child 61260 e6f03fae14d5
     1.1 --- a/src/HOL/Word/Word.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -313,7 +313,7 @@
     1.4    word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
     1.5  
     1.6  instance
     1.7 -  by default (transfer, simp add: algebra_simps)+
     1.8 +  by standard (transfer, simp add: algebra_simps)+
     1.9  
    1.10  end
    1.11  
    1.12 @@ -384,7 +384,7 @@
    1.13    word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
    1.14  
    1.15  instance
    1.16 -  by default (auto simp: word_less_def word_le_def)
    1.17 +  by standard (auto simp: word_less_def word_le_def)
    1.18  
    1.19  end
    1.20  
    1.21 @@ -1194,7 +1194,7 @@
    1.22    by (fact word_less_def)
    1.23  
    1.24  lemma signed_linorder: "class.linorder word_sle word_sless"
    1.25 -  by default (unfold word_sle_def word_sless_def, auto)
    1.26 +  by standard (unfold word_sle_def word_sless_def, auto)
    1.27  
    1.28  interpretation signed: linorder "word_sle" "word_sless"
    1.29    by (rule signed_linorder)
    1.30 @@ -2215,7 +2215,7 @@
    1.31  subsection {* Cardinality, finiteness of set of words *}
    1.32  
    1.33  instance word :: (len0) finite
    1.34 -  by (default, simp add: type_definition.univ [OF type_definition_word])
    1.35 +  by standard (simp add: type_definition.univ [OF type_definition_word])
    1.36  
    1.37  lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
    1.38    by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)