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/Option.thy
changeset 61799 4cf66f21b764
parent 61630 608520e0e8e2
child 63194 0b7bdb75f451 
--- a/src/HOL/Option.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Option.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -15,12 +15,12 @@
 datatype_compat option
 
 lemma [case_names None Some, cases type: option]:
-  -- \<open>for backward compatibility -- names of variables differ\<close>
+  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P"
   by (rule option.exhaust)
 
 lemma [case_names None Some, induct type: option]:
-  -- \<open>for backward compatibility -- names of variables differ\<close>
+  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
   by (rule option.induct)
isabelle