equal
deleted
inserted
replaced
118 \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into |
118 \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into |
119 the current name space of theories. This allows to refer to a theory \<open>A\<close> |
119 the current name space of theories. This allows to refer to a theory \<open>A\<close> |
120 from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again |
120 from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again |
121 into the current ML process, which is in contrast to a theory that is |
121 into the current ML process, which is in contrast to a theory that is |
122 already present in the \<^emph>\<open>parent\<close> session. |
122 already present in the \<^emph>\<open>parent\<close> session. |
|
123 |
|
124 Theories that are imported from other sessions are excluded from the current |
|
125 session document. |
123 |
126 |
124 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
127 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
125 are processed within an environment that is augmented by the given options, |
128 are processed within an environment that is augmented by the given options, |
126 in addition to the global session options given before. Any number of blocks |
129 in addition to the global session options given before. Any number of blocks |
127 of \isakeyword{theories} may be given. Options are only active for each |
130 of \isakeyword{theories} may be given. Options are only active for each |