src/HOL/Library/Mapping.thy
changeset 61585 a9599d3d7610
parent 61076 bdc1e2f0a86a
child 63194 0b7bdb75f451
--- a/src/HOL/Library/Mapping.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -10,7 +10,7 @@
 
 subsection \<open>Parametricity transfer rules\<close>
 
-lemma map_of_foldr: -- \<open>FIXME move\<close>
+lemma map_of_foldr: \<comment> \<open>FIXME move\<close>
   "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
   using map_add_map_of_foldr [of Map.empty] by auto
 
@@ -107,7 +107,7 @@
   is "\<lambda>m k. m k" parametric lookup_parametric .
 
 declare [[code drop: Mapping.lookup]]
-setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close>
+setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
 
 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .