equal
deleted
inserted
replaced
408 |
408 |
409 (* local theories *) |
409 (* local theories *) |
410 |
410 |
411 val _ = |
411 val _ = |
412 Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context" |
412 Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context" |
413 (Parse.position Parse.name --| Parse.begin >> (fn name => |
413 (Parse.position Parse.xname --| Parse.begin >> (fn name => |
414 Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name))); |
414 Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name))); |
415 |
415 |
416 |
416 |
417 (* locales *) |
417 (* locales *) |
418 |
418 |