equal
deleted
inserted
replaced
52 (* ML toplevel use commands *) |
52 (* ML toplevel use commands *) |
53 |
53 |
54 fun use name = Toplevel.program (fn () => Thy_Info.use name); |
54 fun use name = Toplevel.program (fn () => Thy_Info.use name); |
55 fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name); |
55 fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name); |
56 fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name); |
56 fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name); |
57 fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name); |
|
58 fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name); |
|
59 |
57 |
60 |
58 |
61 (* misc *) |
59 (* misc *) |
62 |
60 |
63 val cd = File.cd o Path.explode; |
61 val cd = File.cd o Path.explode; |