# HG changeset patch
# User paulson
# Date 1054287869 -7200
# Node ID dc281bd5ca0aa9c219582b0a81c98f064dfb48c1
# Parent  4daa384f4fd7f58c4093fb3412eb8cc415e1f394
getting ZF/UNITY working again

diff -r 4daa384f4fd7 -r dc281bd5ca0a src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Thu May 29 17:10:00 2003 +0200
+++ b/src/ZF/Nat.thy	Fri May 30 11:44:29 2003 +0200
@@ -290,6 +290,8 @@
 apply (blast intro: lt_trans) 
 done
 
+lemma Le_iff [iff]: "<x,y> : Le <-> x le y & x : nat & y : nat"
+by (force simp add: Le_def)
 
 ML
 {*
diff -r 4daa384f4fd7 -r dc281bd5ca0a src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Thu May 29 17:10:00 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.thy	Fri May 30 11:44:29 2003 +0200
@@ -6,7 +6,7 @@
 Common declarations for Chandy and Charpentier's Allocator
 *)
 
-AllocBase = Follows + MultisetSum + Guar + New +
+AllocBase = Follows + MultisetSum + Guar +
 
 consts
   tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
diff -r 4daa384f4fd7 -r dc281bd5ca0a src/ZF/UNITY/Union.ML
--- a/src/ZF/UNITY/Union.ML	Thu May 29 17:10:00 2003 +0200
+++ b/src/ZF/UNITY/Union.ML	Fri May 30 11:44:29 2003 +0200
@@ -566,11 +566,12 @@
 
 Goal "safety_prop(X) ==> \
 \ (UN G:X. Acts(G)) <= AllowedActs(F) <-> (X <= Allowed(programify(F)))";
-by (auto_tac (claset(), 
-      simpset() addsimps [Allowed_def, 
-              safety_prop_Acts_iff RS iff_sym]));  
+by (asm_full_simp_tac (simpset() addsimps [Allowed_def, 
+              safety_prop_Acts_iff RS iff_sym]) 1);
+by Safe_tac;
+by (REPEAT (Blast_tac 2)); 
 by (rewtac safety_prop_def);
-by Auto_tac;
+by (Blast_tac 1); 
 qed "safety_prop_AllowedActs_iff_Allowed";
 
 
@@ -614,7 +615,8 @@
 
 Goal "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)";
 by (asm_full_simp_tac (simpset() addsimps [safety_prop_def]) 1);
-by Auto_tac; 
+by Safe_tac;
+by (Blast_tac 1); 
 by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
                    ("C", "Union(RepFun(Y, Acts))")] subset_trans 2);
 by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
diff -r 4daa384f4fd7 -r dc281bd5ca0a src/ZF/UNITY/WFair.ML
--- a/src/ZF/UNITY/WFair.ML	Thu May 29 17:10:00 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML	Fri May 30 11:44:29 2003 +0200
@@ -670,7 +670,7 @@
 by (Asm_simp_tac 2);
 by (blast_tac (claset() addSDs [leadsToD2]) 2);
 by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
-by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
+by (blast_tac (claset() addSIs [[asm_rl, wlt_constrains_wlt] 
                                MRS constrains_Un RS constrains_weaken]) 2);
 by (subgoal_tac "F : (W-C) co W" 1);
 by (asm_full_simp_tac (simpset() addsimps  [wlt_increasing RS