| changeset 61580 | c49a8ebd30cc |
| parent 61572 | ddb3ac3fef45 |
| child 61656 | cfabbc083977 |
--- a/src/Doc/Implementation/ML.thy Thu Nov 05 00:02:30 2015 +0100 +++ b/src/Doc/Implementation/ML.thy Thu Nov 05 00:17:13 2015 +0100 @@ -578,7 +578,7 @@ ML_prf %"ML" \<open>val a = 1\<close> { ML_prf %"ML" \<open>val b = a + 1\<close> - } -- \<open>Isar block structure ignored by ML environment\<close> + } \<comment> \<open>Isar block structure ignored by ML environment\<close> ML_prf %"ML" \<open>val c = b + 1\<close> end