--- a/src/ZF/Induct/Rmap.thy Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/Induct/Rmap.thy Thu Jul 23 14:25:05 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1994 University of Cambridge
*)
-section {* An operator to ``map'' a relation over a list *}
+section \<open>An operator to ``map'' a relation over a list\<close>
theory Rmap imports Main begin
@@ -52,10 +52,10 @@
apply blast+
done
-text {*
+text \<open>
\medskip If @{text f} is a function then @{text "rmap(f)"} behaves
as expected.
-*}
+\<close>
lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)