equal
deleted
inserted
replaced
18 |
18 |
19 signature THY_LOAD = |
19 signature THY_LOAD = |
20 sig |
20 sig |
21 include BASIC_THY_LOAD |
21 include BASIC_THY_LOAD |
22 val cond_add_path: Path.T -> ('a -> 'b) -> 'a -> 'b |
22 val cond_add_path: Path.T -> ('a -> 'b) -> 'a -> 'b |
|
23 val ml_exts: string list |
23 val ml_path: string -> Path.T |
24 val ml_path: string -> Path.T |
24 val thy_path: string -> Path.T |
25 val thy_path: string -> Path.T |
25 val check_file: Path.T option -> Path.T -> (Path.T * File.info) option |
26 val check_file: Path.T option -> Path.T -> (Path.T * File.info) option |
26 val load_file: Path.T option -> Path.T -> (Path.T * File.info) |
27 val load_file: Path.T option -> Path.T -> (Path.T * File.info) |
27 eqtype master |
28 eqtype master |