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