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 1 $ 13infixr 3 -->; 14infix 8 via by suffices_by 15infix 9 using 16 17(* infixes for THEN shorthands *) 18infix >> >- >| \\ >>> >>- ?? 19 20infix ~~ !~ Un Isct -- IN -* 21 22signature KERNEL = 23sig 24 structure Tag : FinalTag 25 structure Type : FinalType 26 structure Term : FinalTerm where type hol_type = Type.hol_type 27 structure Net : FinalNet where type term = Term.term 28 structure Thm : Thm where type tag = Tag.tag 29 and type hol_type = Type.hol_type 30 and type term = Term.term 31end 32 33structure Kernel :> KERNEL = 34struct 35 structure Tag = Tag 36 structure Type = Type 37 structure Term = Term 38 structure Net = Net 39 structure Thm = Thm 40end 41 42open Kernel 43 44structure Process = OS.Process 45structure FileSys = OS.FileSys 46structure Path = OS.Path 47 48type 'a quotation = 'a HOLPP.quotation 49datatype frag = datatype HOLPP.frag 50structure PP = HOLPP 51