# HG changeset patch
# User paulson
# Date 904725382 -7200
# Node ID 578dc167453f6cbafe489cfd46f4b924eaba35ca
# Parent  01fc8d6a40f2ae424595ee4cadd3149a5495acb7
Moved constrains_tac from SubstAx to Constrains.
Removed Auto_tac calls from it and ensures_tac

diff -r 01fc8d6a40f2 -r 578dc167453f src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Wed Sep 02 10:35:11 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Wed Sep 02 10:36:22 1998 +0200
@@ -252,4 +252,19 @@
 val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
 
 
+(** main_def defines the main program as a set;
+    cmd_defs defines the separate commands
+**)
 
+(*proves "constrains" properties when the program is specified*)
+fun constrains_tac (main_def::cmd_defs) = 
+   SELECT_GOAL
+      (EVERY [REPEAT (resolve_tac [StableI, stableI,
+				   constrains_imp_Constrains] 1),
+	      rtac constrainsI 1,
+	      full_simp_tac (simpset() addsimps [main_def]) 1,
+	      REPEAT_FIRST (etac disjE),
+	      ALLGOALS Clarify_tac,
+	      ALLGOALS (asm_full_simp_tac (simpset() addsimps cmd_defs))]);
+
+
diff -r 01fc8d6a40f2 -r 578dc167453f src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Wed Sep 02 10:35:11 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Wed Sep 02 10:36:22 1998 +0200
@@ -401,23 +401,10 @@
 qed "Finite_completion";
 
 
-(** Constrains/Ensures tactics 
-    main_def defines the main program as a set;
+(** main_def defines the main program as a set;
     cmd_defs defines the separate commands
 **)
 
-(*proves "constrains" properties when the program is specified*)
-fun constrains_tac (main_def::cmd_defs) = 
-   SELECT_GOAL
-      (EVERY [REPEAT (resolve_tac [StableI, stableI,
-				   constrains_imp_Constrains] 1),
-	      rtac constrainsI 1,
-	      full_simp_tac (simpset() addsimps [main_def]) 1,
-	      REPEAT_FIRST (etac disjE ),
-	      rewrite_goals_tac cmd_defs,
-	      ALLGOALS (SELECT_GOAL Auto_tac)]);
-
-
 (*proves "ensures/leadsTo" properties when the program is specified*)
 fun ensures_tac (main_def::cmd_defs) sact = 
     SELECT_GOAL
@@ -433,6 +420,6 @@
 	      constrains_tac (main_def::cmd_defs) 1,
 	      rewrite_goals_tac cmd_defs,
 	      ALLGOALS Clarify_tac,
-	      Auto_tac]);
+	      ALLGOALS Asm_full_simp_tac]);