--- 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";