--- a/IOA/example/Correctness.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Correctness.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Correctness.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
open Impl;
open Spec;
@@ -28,13 +36,12 @@
\ | C_r_s => False \
\ | C_r_r(m) => False)";
by(simp_tac (hom_ss addcongs [if_weak_cong]
- addsimps ([asig_projections_def,externals_def,
- restrict_def,restrict_asig_def,
- asig_of_par, asig_comp_def, Spec.sig_def]
- @ impl_ioas @ impl_asigs)) 1);
- by(Action.action.induct_tac "a" 1);
+ addsimps ([externals_def, restrict_def, restrict_asig_def,
+ asig_of_par, asig_comp_def, Spec.sig_def] @
+ asig_projections @ impl_ioas @ impl_asigs)) 1);
+ by(Action.action.induct_tac "a" 1);
by(ALLGOALS(simp_tac (action_ss addsimps
- (actions_def :: asig_projections_def :: set_lemmas))));
+ (actions_def :: asig_projections @ set_lemmas))));
val externals_lemma = result();