--- a/src/HOL/UNITY/Lift_prog.ML Tue Sep 21 11:09:24 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Tue Sep 21 11:11:09 1999 +0200
@@ -245,8 +245,10 @@
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
by (simp_tac (simpset()
- addsimps [lift_export Acts_project,
- drop_act_correct]) 1);
+ addsimps [Acts_project, drop_act_correct]) 1);
+by (rtac (insert_absorb RS sym) 1);
+by (rtac (Id_in_Acts RSN (2,image_eqI)) 1);
+by (rtac (project_set_UNIV RS lift_export project_act_Id RS sym) 1);
qed "drop_prog_correct";