# HG changeset patch # User traytel # Date 1382444526 -7200 # Node ID 7bbe8209c253b23d44cc14ee684c4297db8380e3 # Parent c0186a0d8cb3265a2f137ef7c74b41b14eabf078 update doc according to c0186a0d8cb3 diff -r c0186a0d8cb3 -r 7bbe8209c253 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 22 14:17:12 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 22 14:22:06 2013 +0200 @@ -2233,7 +2233,7 @@ @{rail " @@{command bnf} target? (name ':')? term \\ - term_list term term_list term? + term_list term term_list? term? ; X_list: '[' (X + ',') ']' "}