# HG changeset patch # User blanchet # Date 1380035166 -7200 # Node ID 408c9a3617e36a46bcffed27f31e1a309c9ffc3a # Parent 62c2f66ff9b2076f14d3a039dec2d5236537e83e improved rail diagram diff -r 62c2f66ff9b2 -r 408c9a3617e3 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 16:59:14 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 17:06:06 2013 +0200 @@ -2023,10 +2023,10 @@ Primitive corecursive definitions have the following general syntax: @{rail " - (@@{command_def primcorec} | @@{command_def primcorecursive}) target? @{syntax pcr_option}? fixes \\ @'where' + (@@{command_def primcorec} | @@{command_def primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where' (@{syntax pcr_formula} + '|') ; - @{syntax_def pcr_option}: '(' 'sequential' | 'exhaustive' ')' + @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')' ; @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))? "}