| changeset 71760 | e4e05fcd8937 |
| parent 71535 | b612edee9b0c |
| child 71822 | 67cc2319104f |
--- a/src/HOL/ex/Word.thy Thu Apr 16 08:09:31 2020 +0200 +++ b/src/HOL/ex/Word.thy Thu Apr 16 08:09:32 2020 +0200 @@ -157,7 +157,7 @@ by transfer_prover lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral" + "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len0 word \<Rightarrow> bool)) numeral numeral" by transfer_prover lemma [transfer_rule]: