--- a/src/HOL/IMP/Expr.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/IMP/Expr.ML Mon Jun 22 17:26:46 1998 +0200
@@ -32,14 +32,14 @@
"((b0 ori b1,sigma) -b-> w) = \
\ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
-goal Expr.thy "!n. ((a,s) -a-> n) = (A a s = n)";
+Goal "!n. ((a,s) -a-> n) = (A a s = n)";
by (aexp.induct_tac "a" 1);
by (ALLGOALS
(fast_tac (claset() addSIs evala.intrs
addSEs evala_elim_cases addss (simpset()))));
qed_spec_mp "aexp_iff";
-goal Expr.thy "!w. ((b,s) -b-> w) = (B b s = w)";
+Goal "!w. ((b,s) -b-> w) = (B b s = w)";
by (bexp.induct_tac "b" 1);
by (ALLGOALS
(fast_tac (claset()