equal
deleted
inserted
replaced
101 @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
101 @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
102 @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\ |
102 @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\ |
103 \end{matharray} |
103 \end{matharray} |
104 |
104 |
105 @{rail " |
105 @{rail " |
106 @@{command context} @{syntax name} @'begin' |
106 @@{command context} @{syntax nameref} @'begin' |
107 ; |
107 ; |
108 |
108 |
109 @{syntax_def target}: '(' @'in' @{syntax name} ')' |
109 @{syntax_def target}: '(' @'in' @{syntax nameref} ')' |
110 "} |
110 "} |
111 |
111 |
112 \begin{description} |
112 \begin{description} |
113 |
113 |
114 \item @{command "context"}~@{text "c \<BEGIN>"} recommences an |
114 \item @{command "context"}~@{text "c \<BEGIN>"} recommences an |