| changeset 55442 | 17fb554688f0 |
| parent 55417 | 01fbfb60c33e |
| child 55466 | 786edc984c98 |
--- a/src/HOL/Option.thy Wed Feb 12 16:35:58 2014 +0100 +++ b/src/HOL/Option.thy Wed Feb 12 17:35:59 2014 +0100 @@ -24,7 +24,8 @@ "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option" by (rule option.induct) --- {* Compatibility *} +text {* Compatibility: *} + setup {* Sign.mandatory_path "option" *} lemmas inducts = option.induct