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