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/Word/Word.thy
changeset 72102 0b21b2beadb5
parent 72088 a36db1c8238e
child 72128 3707cf7b370b 
--- a/src/HOL/Word/Word.thy	Thu Aug 06 17:51:37 2020 +0200
+++ b/src/HOL/Word/Word.thy	Thu Aug 06 15:37:14 2020 +0000
@@ -415,11 +415,11 @@
 begin
 
 lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
+  "((=) ===> pcr_word) of_bool of_bool"
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
+  "((=) ===> pcr_word) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
isabelle