src/HOL/Isar_examples/ExprCompiler.thy
changeset 7982 d534b897ce39
parent 7874 180364256231
child 8031 826c6222cca2
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Oct 30 20:13:16 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Oct 30 20:20:48 1999 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  text {*
     1.6   Binary operations are just functions over some type of values.  This
     1.7 - is both for syntax and semantics, i.e.\ we use a ``shallow
     1.8 + is both for abstract syntax and semantics, i.e.\ we use a ``shallow
     1.9   embedding'' here.
    1.10  *};
    1.11