equal
deleted
inserted
replaced
15 end; |
15 end; |
16 |
16 |
17 signature THY_LOAD = |
17 signature THY_LOAD = |
18 sig |
18 sig |
19 include BASIC_THY_LOAD |
19 include BASIC_THY_LOAD |
|
20 val cond_with_path: Path.T -> ('a -> 'b) -> 'a -> 'b |
20 val ml_path: string -> Path.T |
21 val ml_path: string -> Path.T |
21 val thy_path: string -> Path.T |
22 val thy_path: string -> Path.T |
22 val check_file: Path.T -> (Path.T * File.info) option |
23 val check_file: Path.T -> (Path.T * File.info) option |
23 val load_file: Path.T -> (Path.T * File.info) |
24 val load_file: Path.T -> (Path.T * File.info) |
24 eqtype master |
25 eqtype master |