| changeset 39866 | 5ec01d5acd0c |
| parent 39846 | cb6634eb8926 |
| child 40110 | 93e7935d4cb5 |
--- a/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 18 16:23:55 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 18 19:06:07 2010 +0100 @@ -3,4 +3,10 @@ uses "../../antiquote_setup.ML" begin +(* FIXME move to src/Pure/ML/ml_antiquote.ML *) +ML {* + ML_Antiquote.inline "assert" + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") +*} + end