src/HOL/HOL.thy
changeset 41229 d797baa3d57c
parent 41184 5c6f44d22f51
child 41251 1e6d86821718
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 17 17:08:56 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Dec 17 17:43:54 2010 +0100
     1.3 @@ -103,9 +103,8 @@
     1.4  notation (xsymbols)
     1.5    iff  (infixr "\<longleftrightarrow>" 25)
     1.6  
     1.7 -nonterminals
     1.8 -  letbinds  letbind
     1.9 -  case_syn  cases_syn
    1.10 +nonterminal letbinds and letbind
    1.11 +nonterminal case_syn and cases_syn
    1.12  
    1.13  syntax
    1.14    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)