[isabelle-dev] NEWS: 'corec' command

Jasmin Blanchette jasmin.blanchette at inria.fr
Mon Apr 4 09:47:18 CEST 2016


*** 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



More information about the isabelle-dev mailing list