# HG changeset patch
# User paulson
# Date 906538278 -7200
# Node ID 130f3d891fb258f044ad4fdd1e7a1dd117cab916
# Parent  678999604ee98266d8c9be2f675f9bb6c4860553
tidying and deleting needless parentheses

diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -217,6 +217,8 @@
 			 Int_assoc RS sym]) 1);
 qed "Invariant_ConstrainsI";
 
+(* [| Invariant prg INV; Constrains prg (INV Int A) A |]
+   ==> Stable prg A *)
 bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
 
 Goal "[| Invariant prg INV;  Constrains prg A A' |]   \
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -66,9 +66,9 @@
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac
-    (simpset() addsimps (Int_ac @
-			 [Int_Un_distrib, Int_Un_distrib2, lemma,
-			  Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
+    (simpset() addsimps Int_ac @
+			[Int_Un_distrib, Int_Un_distrib2, lemma,
+			 Collect_less_Suc_insert, Collect_le_Suc_insert]) 1);
 qed "INT_le_equals_Int";
 
 Goal "(INT i:{i. i <= Suc n}. A i) = \
@@ -88,6 +88,6 @@
     constrains_Int RS constrains_weaken) 1);
 by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
 				  Int_assoc, INT_absorb]) 1);
-by (simp_tac (simpset() addsimps ([INT_le_Suc_equals_Int])) 1);
+by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
 result();
 
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/LessThan.thy
--- a/src/HOL/UNITY/LessThan.thy	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/LessThan.thy	Wed Sep 23 10:11:18 1998 +0200
@@ -4,6 +4,8 @@
     Copyright   1998  University of Cambridge
 
 lessThan, greaterThan, atLeast, atMost
+
+Could generalize to any linear ordering?
 *)
 
 LessThan = Main +
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -31,9 +31,9 @@
 by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
 by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
 by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
-br reachable.Init 5;
+by (rtac reachable.Init 5);
 by (ALLGOALS Asm_simp_tac);
-by (REPEAT_FIRST (resolve_tac [exI]));
+by (REPEAT_FIRST (rtac exI ));
 by possibility_tac;
 result();
 
@@ -75,7 +75,7 @@
 *)
 
 Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)";
-be reachable.induct 1;
+by (etac reachable.induct 1);
 by Auto_tac;
 qed "Spy_see_priK";
 Addsimps [Spy_see_priK];
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -113,7 +113,7 @@
 by (ensures_tac "asgt a b" 1);
 by (Blast_tac 2);
 by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
-bd (metric_le RS le_anti_sym) 1;
+by (dtac (metric_le RS le_anti_sym) 1);
 by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
 	      simpset()));
 qed "LeadsTo_Diff_fixedpoint";
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -267,7 +267,7 @@
 
 Goal "[| LeadsTo prg A A'; Stable prg B |] \
 \     ==> LeadsTo prg (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
 qed "PSP_stable2";
 
 Goalw [LeadsTo_def, Constrains_def]
@@ -278,7 +278,7 @@
 
 Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
 \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
 qed "PSP2";
 
 Goalw [Unless_def]
diff -r 678999604ee9 -r 130f3d891fb2 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -281,7 +281,7 @@
 
 Goal "[| leadsTo acts A A'; stable acts B |] \
 \   ==> leadsTo acts (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (psp_stable::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
 qed "psp_stable2";
 
 Goalw [ensures_def, constrains_def]
@@ -306,7 +306,7 @@
 
 Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
 \   ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (psp::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
 qed "psp2";