# HG changeset patch
# User paulson
# Date 937905069 -7200
# Node ID a72a551b6d795ed0bfd10927c4de1076b7f74af7
# Parent  36b26759147e5a79ac321999bde4b6ba470e780f
new proof of drop_prog_correct for new definition of project_act

diff -r 36b26759147e -r a72a551b6d79 src/HOL/UNITY/Lift_prog.ML
--- 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";