doc-src/IsarImplementation/Thy/Base.thy
author wenzelm
Fri, 22 Oct 2010 19:03:31 +0100
changeset 39882 ab0afd03a042
parent 39866 5ec01d5acd0c
child 40110 93e7935d4cb5
permissions -rw-r--r--
cover @{Isar.state};

theory Base
imports Main
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