diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Correctness.ML
--- 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();