equal
deleted
inserted
replaced
130 returns the resulting theory, after applying the resulting facts to the |
130 returns the resulting theory, after applying the resulting facts to the |
131 target context. |
131 target context. |
132 \<close> |
132 \<close> |
133 |
133 |
134 text %mlex \<open> |
134 text %mlex \<open> |
135 The file @{file "~~/src/HOL/ex/Commands.thy"} shows some example Isar |
135 The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command |
136 command definitions, with the all-important theory header declarations for |
136 definitions, with the all-important theory header declarations for outer |
137 outer syntax keywords. |
137 syntax keywords. |
138 \<close> |
138 \<close> |
139 |
139 |
140 |
140 |
141 section \<open>Theory loader database\<close> |
141 section \<open>Theory loader database\<close> |
142 |
142 |