src/HOL/Option.thy
changeset 4192 c38ab5af38b5
parent 4133 0a08c2b9b1ed
child 4752 1c334bd00038
     1.1 --- a/src/HOL/Option.thy	Mon Nov 10 14:30:35 1997 +0100
     1.2 +++ b/src/HOL/Option.thy	Mon Nov 10 14:57:31 1997 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4  constdefs
     1.5  
     1.6    the		:: "'a option => 'a"
     1.7 - "the  %y. case y of None => arbitrary | Some x => x"
     1.8 + "the == %y. case y of None => arbitrary | Some x => x"
     1.9  
    1.10    option_map	:: "('a => 'b) => ('a option => 'b option)"
    1.11 - "option_map  %f y. case y of None => None | Some x => Some (f x)"
    1.12 + "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.13  
    1.14  end