eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord
% This file was generated by 'rail' from 'logics.rai'
\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
\rail@o {1}{
\rail@begin{2}{typedef}
\rail@term{typedef}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{name}[]
\rail@term{)}[]
\rail@endbar
\rail@nont{type}[]
\rail@term{=}[]
\rail@nont{set}[]
\rail@nont{witness}[]
\rail@end
\rail@begin{2}{type}
\rail@nont{typevarlist}[]
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{infix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{1}{set}
\rail@nont{string}[]
\rail@end
\rail@begin{2}{witness}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}
\rail@i {2}{ typedecl : typevarlist id '=' (cons + '|') ; cons : name (typ *) ( () | mixfix ) ; typ : id | tid | ('(' typevarlist id ')') ; }
\rail@o {2}{
\rail@begin{2}{typedecl}
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@term{=}[]
\rail@plus
\rail@nont{cons}[]
\rail@nextplus{1}
\rail@cterm{|}[]
\rail@endplus
\rail@end
\rail@begin{3}{cons}
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
\rail@nont{typ}[]
\rail@nextplus{2}
\rail@endplus
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{mixfix}[]
\rail@endbar
\rail@end
\rail@begin{3}{typ}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@nont{tid}[]
\rail@nextbar{2}
\rail@term{(}[]
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}