# HG changeset patch # User wenzelm # Date 924879696 -7200 # Node ID 914729515c265781fb6fb96efae39d22c7ca4470 # Parent bc30e13b36a8aacd5c404ca5e4a78c1967a24aba tuned antiquotations; diff -r bc30e13b36a8 -r 914729515c26 src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Fri Apr 23 16:38:22 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Fri Apr 23 17:01:36 1999 +0200 @@ -16,7 +16,7 @@ text {| First we define a type abbreviation for binary operations over some - type @type "'val" of values. + type @{type "'val"} of values. |}; types @@ -98,7 +98,7 @@ text {| The main result of this developement is the correctness theorem for - @term "comp". We first establish some lemmas. + @{term "comp"}. We first establish some lemmas. |}; ML "reset HOL_quantifiers";