# HG changeset patch
# User paulson
# Date 831564632 -7200
# Node ID 2ad693c6cb134ce61dc393c9f685da3acde1e90d
# Parent  1c7f793fc3748077b7a425154df087425fae83fa
Updated for new form of induction rules

diff -r 1c7f793fc374 -r 2ad693c6cb13 src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Tue May 07 18:19:13 1996 +0200
+++ b/src/HOL/IMP/Denotation.ML	Wed May 08 16:10:32 1996 +0200
@@ -33,10 +33,10 @@
 
 (* Operational Semantics implies Denotational Semantics *)
 
-goal Denotation.thy "!c s t. <c,s> -c-> t --> (s,t) : C(c)";
+goal Denotation.thy "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)";
 
 (* start with rule induction *)
-by (rtac evalc.mutual_induct 1);
+by (etac evalc.induct 1);
 by (rewrite_tac (Gamma_def::C_simps));
   (* simplification with HOL_ss too agressive *)
 (* skip *)
@@ -54,7 +54,7 @@
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
 by (fast_tac denotation_cs 1);
 
-qed_spec_mp "com1";
+qed "com1";
 
 
 (* Denotational Semantics implies Operational Semantics *)