changeset 35841 | 94f901e4969a |
parent 35757 | 93603d7b8ee9 |
child 36137 | 0c2538afe8e8 |
1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Mar 19 00:43:49 2010 +0100 1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Mar 19 00:46:08 2010 +0100 1.3 @@ -37,7 +37,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 ;