equal
deleted
inserted
replaced
253 fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory; |
253 fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory; |
254 |
254 |
255 |
255 |
256 (* context switch *) |
256 (* context switch *) |
257 |
257 |
258 fun switch_theory require name = |
258 fun switch_theory load name = |
259 Toplevel.init_theory |
259 Toplevel.init_theory |
260 (fn () => (Context.save require name; ThyInfo.get_theory name)) (K ()); |
260 (fn () => (Context.save load name; ThyInfo.get_theory name)) (K ()); |
261 |
261 |
262 val context = switch_theory ThyInfo.use_thy; |
262 val context = switch_theory ThyInfo.use_thy; |
263 val update_context = switch_theory ThyInfo.update_thy; |
263 val update_context = switch_theory ThyInfo.update_thy; |
264 |
264 |
265 |
265 |