src/HOL/Product_Type.thy
changeset 41229 d797baa3d57c
parent 40968 a6fcd305f7dc
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Product_Type.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -173,8 +173,7 @@
     1.4    abstractions.
     1.5  *}
     1.6  
     1.7 -nonterminals
     1.8 -  tuple_args patterns
     1.9 +nonterminal tuple_args and patterns
    1.10  
    1.11  syntax
    1.12    "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")