--- a/doc-src/HOL/logics-HOL.rai Mon May 02 21:33:21 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\rail@i{1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
-type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
-\rail@i{2}{ datatype : 'datatype' typedecls; \par
-typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }