1(* ----------------------------------------------------------------------
2    Provide standard infixes for rest of distribution
3
4    These infix declarations affect the interactive system as well as
5    the "compiled" environment, ensuring a degree of consistency
6    between the two.
7   ---------------------------------------------------------------------- *)
8
9infix ++ && |-> THEN THEN1 THENL THEN_LT THENC ORELSE ORELSE_LT ORELSEC
10  THEN_TCL ORELSE_TCL ?> |> |>> ||> ||->
11infixr ## $ ?
12infixr 3 -->;
13infix 8 via by suffices_by
14
15(* infixes for THEN shorthands *)
16infix >> >- >| \\ >>> >>- ??
17
18infix ~~ !~ Un Isct -- IN
19
20structure Tag = Tag :> FinalTag where type tag = Tag.tag
21structure Type = Type :> FinalType where type hol_type = Type.hol_type
22structure Term = Term :> FinalTerm where type term = Term.term
23                                         and type hol_type = Type.hol_type
24
25structure Process = OS.Process
26structure FileSys = OS.FileSys
27structure Path    = OS.Path
28
29type 'a quotation = 'a HOLPP.quotation
30datatype frag = datatype HOLPP.frag
31structure PP = HOLPP
32