changeset 67399 | eab6ce8368fa |
parent 66453 | cc19f7ca2ed6 |
--- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy Wed Jan 10 15:25:09 2018 +0100 @@ -149,7 +149,7 @@ consts integerize_tree_list :: "'a list \<Rightarrow> int" lemma integerize_tree_list_transfer[transfer_rule]: - "rel_fun (list_all2 R) op = integerize_tree_list integerize_tree_list" + "rel_fun (list_all2 R) (=) integerize_tree_list integerize_tree_list" sorry corec (friend) f10a where