--- a/src/HOL/Induct/Exp.thy Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/Induct/Exp.thy Wed Oct 21 17:48:02 1998 +0200
@@ -27,7 +27,7 @@
valOf "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |]
==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
- monos "[exec_mono]"
+ monos exec_mono
end