*** HOL ***
* (Co)datatype package:
- New commands for defining corecursive functions and reasoning about
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
method. See 'isabelle doc corec'.
This refers to db9f95ca2a8f.
Jasmin