diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Mon Aug 03 14:01:57 2009 +0200 +++ b/ProgTutorial/Base.thy Mon Aug 03 16:47:01 2009 +0200 @@ -6,6 +6,7 @@ "antiquote_setup.ML" begin +(* re-definition of various ML antiquotations *) (* to have a special tag for text enclosed in ML *) ML {*