equal
deleted
inserted
replaced
259 |
259 |
260 lemma "A \<and> B \<longrightarrow> B \<and> A" |
260 lemma "A \<and> B \<longrightarrow> B \<and> A" |
261 by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+) |
261 by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+) |
262 |
262 |
263 |
263 |
264 subsection \<open>ML syntax: input source\<close> |
264 subsection \<open>ML syntax\<close> |
265 |
265 |
|
266 text \<open>Input source with position information:\<close> |
266 ML \<open> |
267 ML \<open> |
267 val s: Input.source = \<open>abc\<close>; |
268 val s: Input.source = \<open>abc\<close>; |
268 writeln ("Look here!" ^ Position.here (Input.pos_of s)); |
269 writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s))); |
269 |
270 |
270 \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) => |
271 \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) => |
271 if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); |
272 if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); |
272 \<close> |
273 \<close> |
273 |
274 |
|
275 text \<open>Nested ML evaluation:\<close> |
|
276 ML \<open> |
|
277 val ML = ML_Context.eval_source ML_Compiler.flags; |
|
278 |
|
279 ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>; |
|
280 ML \<open>val b = @{thm sym}\<close>; |
|
281 val c = @{thm trans} |
|
282 val thms = [a, b, c]; |
|
283 \<close> |
|
284 |
|
285 ML \<open>\<close> |
|
286 |
274 end |
287 end |