# HG changeset patch
# User paulson
# Date 924611568 -7200
# Node ID bc943acc5fdaedbab3187b89cbf8608b4690d20c
# Parent  990e6e2dee2645dce42a29caaeb18f0aee1bcd52
tidied

diff -r 990e6e2dee26 -r bc943acc5fda src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Apr 19 17:53:38 1999 +0200
+++ b/src/HOL/List.ML	Tue Apr 20 14:32:48 1999 +0200
@@ -333,13 +333,11 @@
 qed "rev_map";
 
 (* a congruence rule for map: *)
-Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
-by (rtac impI 1);
+Goal "xs=ys ==> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
 by (hyp_subst_tac 1);
 by (induct_tac "ys" 1);
 by Auto_tac;
-val lemma = result();
-bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
+bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
 Goal "(map f xs = []) = (xs = [])";
 by (induct_tac "xs" 1);
diff -r 990e6e2dee26 -r bc943acc5fda src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Mon Apr 19 17:53:38 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Tue Apr 20 14:32:48 1999 +0200
@@ -21,12 +21,6 @@
 qed "lift_act_Id";
 Addsimps [lift_act_Id];
 
-(*NEEDED????????????????????????????????????????????????????????????????*)
-Goal "Id : lift_act i `` Acts F";
-by (auto_tac (claset() addSIs [lift_act_Id RS sym], 
-	      simpset() addsimps [image_iff]));
-qed "Id_mem_lift_act";
-
 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
 by Auto_tac;
 qed "Init_lift_prog";
@@ -133,19 +127,12 @@
 
 (** invariant **)
 
-(*????????????????*)
-Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)";
+(*UNUSED*)
+Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
-qed "invariant_imp_lift_prog_invariant";
+qed "lift_prog_invariant_eq";
 
-(*????????????????*)
-Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A";
-by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
-qed "lift_prog_invariant_imp_invariant";
-
-(*NOT clear that the previous lemmas help in proving this one.*)
 Goal "[| F i : invariant A;  i : I |] \
 \     ==> PPROD I F : invariant (lift_set i A)";
 by (auto_tac (claset(),
diff -r 990e6e2dee26 -r bc943acc5fda src/HOL/ex/Recdefs.ML
--- a/src/HOL/ex/Recdefs.ML	Mon Apr 19 17:53:38 1999 +0200
+++ b/src/HOL/ex/Recdefs.ML	Tue Apr 20 14:32:48 1999 +0200
@@ -11,8 +11,7 @@
 
 Goal "(x: set (qsort (ord,l))) = (x: set l)";
 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
+by Auto_tac;
 qed "qsort_mem_stable";
 
 
diff -r 990e6e2dee26 -r bc943acc5fda src/Sequents/ILL.ML
--- a/src/Sequents/ILL.ML	Mon Apr 19 17:53:38 1999 +0200
+++ b/src/Sequents/ILL.ML	Tue Apr 20 14:32:48 1999 +0200
@@ -5,9 +5,6 @@
 
 *)
 
-open ILL;
-
-
 val lazy_cs = empty_pack
  add_safes [tensl, conjr, disjl, promote0,
 	    context2,context3]