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 55417 01fbfb60c33e
parent 55414 eab03e9cee8a
child 55442 17fb554688f0 
--- a/src/HOL/Option.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Option.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -16,7 +16,7 @@
 
 lemma [case_names None Some, cases type: option]:
   -- {* for backward compatibility -- names of variables differ *}
-  "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>option. y = Some option \<Longrightarrow> P) \<Longrightarrow> P"
+  "(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]:
isabelle