changeset 56995 | 61855ade6c7e |
parent 56992 | d0e5225601d3 |
child 57047 | 90d4db566e12 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:44:13 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:53:58 2014 +0200 @@ -194,7 +194,7 @@ *} (*<*) - hide_const None Some + hide_const None Some map_option hide_type option (*>*) datatype_new 'a option = None | Some 'a @@ -367,7 +367,7 @@ Cons (infixr "#" 65) hide_type list - hide_const Nil Cons hd tl set map list_all2 + hide_const Nil Cons hd tl set map list_all2 rec_list size_list context early begin (*>*)