equal
deleted
inserted
replaced
175 Again the function @{ML commas} helps with printing more than one theorem. |
175 Again the function @{ML commas} helps with printing more than one theorem. |
176 *} |
176 *} |
177 |
177 |
178 ML{*fun str_of_thms ctxt thms = |
178 ML{*fun str_of_thms ctxt thms = |
179 commas (map (str_of_thm ctxt) thms)*} |
179 commas (map (str_of_thm ctxt) thms)*} |
|
180 |
|
181 text {* |
|
182 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug}) |
|
183 *} |
180 |
184 |
181 section {* Combinators\label{sec:combinators} *} |
185 section {* Combinators\label{sec:combinators} *} |
182 |
186 |
183 text {* |
187 text {* |
184 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 |