src/HOL/HOL.thy
changeset 41251 1e6d86821718
parent 41247 c5cb19ecbd41
parent 41229 d797baa3d57c
child 41636 934b4ad9b611
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 17 18:24:44 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Dec 17 18:33:35 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)