doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 35841 94f901e4969a
parent 35757 93603d7b8ee9
child 36137 0c2538afe8e8
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:43:49 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:46:08 2010 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5      altname: '(' (name | 'open' | 'open' name) ')'
     1.6      ;
     1.7 -    abstype: typespec mixfix?
     1.8 +    abstype: typespecsorts mixfix?
     1.9      ;
    1.10      repset: term ('morphisms' name name)?
    1.11      ;