--- a/src/HOL/IMP/Expr.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Expr.thy Fri Jul 24 13:03:20 1998 +0200
@@ -7,7 +7,7 @@
Not used in the rest of the language, but included for completeness.
*)
-Expr = Arith + Inductive +
+Expr = Datatype +
(** Arithmetic expressions **)
types loc
@@ -72,13 +72,13 @@
A :: aexp => state => nat
B :: bexp => state => bool
-primrec A aexp
+primrec
"A(N(n)) = (%s. n)"
"A(X(x)) = (%s. s(x))"
"A(Op1 f a) = (%s. f(A a s))"
"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-primrec B bexp
+primrec
"B(true) = (%s. True)"
"B(false) = (%s. False)"
"B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"