152 ML{*fun str_of_cterms ctxt ts = |
152 ML{*fun str_of_cterms ctxt ts = |
153 commas (map (str_of_cterm ctxt) ts)*} |
153 commas (map (str_of_cterm ctxt) ts)*} |
154 |
154 |
155 text {* |
155 text {* |
156 The easiest way to get the string of a theorem is to transform it |
156 The easiest way to get the string of a theorem is to transform it |
157 into a @{ML_type cterm} using the function @{ML crep_thm}. |
157 into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems |
158 *} |
158 also include schematic variables, such as @{text "?P"}, @{text "?Q"} |
159 |
159 and so on. In order to improve the readability of theorems we convert |
160 ML{*fun str_of_thm ctxt thm = |
160 these schematic variables into free variables using the |
161 let |
161 function @{ML Variable.import_thms}. |
162 val {prop, ...} = crep_thm thm |
162 *} |
163 in |
163 |
164 str_of_cterm ctxt prop |
164 ML{*fun no_vars ctxt thm = |
165 end*} |
165 let |
|
166 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt |
|
167 in |
|
168 thm' |
|
169 end |
|
170 |
|
171 fun str_of_thm ctxt thm = |
|
172 let |
|
173 val {prop, ...} = crep_thm (no_vars ctxt thm) |
|
174 in |
|
175 str_of_cterm ctxt prop |
|
176 end*} |
166 |
177 |
167 text {* |
178 text {* |
168 Again the function @{ML commas} helps with printing more than one theorem. |
179 Again the function @{ML commas} helps with printing more than one theorem. |
169 *} |
180 *} |
170 |
181 |
171 ML{*fun str_of_thms ctxt thms = |
182 ML{*fun str_of_thms ctxt thms = |
172 commas (map (str_of_thm ctxt) thms)*} |
183 commas (map (str_of_thm ctxt) thms)*} |
173 |
|
174 |
184 |
175 section {* Combinators\label{sec:combinators} *} |
185 section {* Combinators\label{sec:combinators} *} |
176 |
186 |
177 text {* |
187 text {* |
178 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
188 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |