src/HOL/Option.thy
changeset 55867 79b915f26533
parent 55531 601ca8efa000
child 57091 1fa9c19ba2c9
     1.1 --- a/src/HOL/Option.thy	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/src/HOL/Option.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -28,7 +28,6 @@
     1.4  setup {* Sign.mandatory_path "option" *}
     1.5  
     1.6  lemmas inducts = option.induct
     1.7 -lemmas recs = option.rec
     1.8  lemmas cases = option.case
     1.9  
    1.10  setup {* Sign.parent_path *}