# HG changeset patch
# User paulson
# Date 942312329 -3600
# Node ID 299127ded09d53ecfeca4ca72533199b98006598
# Parent  b64d8601878546d14e4c829612b315737edd08d1
tidied

diff -r b64d86018785 -r 299127ded09d src/HOL/Algebra/abstract/NatSum.ML
--- a/src/HOL/Algebra/abstract/NatSum.ML	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/Algebra/abstract/NatSum.ML	Thu Nov 11 10:25:29 1999 +0100
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 12 December 1996
 *)
 
-open NatSum;
-
 section "Basic Properties";
 
 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
@@ -164,12 +162,12 @@
 \    SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
 by (nat_ind_tac "n" 1);
 (* Base case *)
-by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
 (* Induction step *)
-by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Asm_simp_tac 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("f", "f")] arg_cong 1);
-by (fast_arith_tac 1);
+by (arith_tac 1);
 qed "SUM_if_singleton";
 
 Goal
diff -r b64d86018785 -r 299127ded09d src/HOL/Algebra/poly/Degree.ML
--- a/src/HOL/Algebra/poly/Degree.ML	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/Algebra/poly/Degree.ML	Thu Nov 11 10:25:29 1999 +0100
@@ -285,7 +285,7 @@
 by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
 by (auto_tac
   (claset() addDs [not_leE],
-   simpset() setloop (split_tac [expand_if])));
+   simpset()));
 qed "bound_SUM_if";
 
 Goal
@@ -297,8 +297,7 @@
 by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
 by (rtac SUM_cong 1);
 by (rtac refl 1);
-by (asm_simp_tac 
-  (simpset() setloop (split_tac [expand_if])) 1);
+by (Asm_simp_tac 1);
 qed "up_repr";
 
 Goal
diff -r b64d86018785 -r 299127ded09d src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Thu Nov 11 10:25:29 1999 +0100
@@ -4,29 +4,6 @@
     Author: Clemens Ballarin, started 23 June 1999
 *)
 
-open LongDiv;
-
-(*
-Goalw [lcoeff_def]
-  "!!p::('a::ring up). \
-\    [| deg p = deg q; lcoeff p = - (lcoeff q); deg q ~= 0 |] ==> \
-\       deg (p + q) < deg q";
-by (res_inst_tac [("j", "deg q - 1")] le_less_trans 1);
-by (rtac deg_aboveI 1);
-by (strip_tac 1);
-by (dtac pred_less_imp_le 1);
-by (case_tac "deg q = m" 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-(* case "deg q ~= m" *)
-by (dtac le_neq_implies_less 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-(* end case *)
-by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
-qed "deg_lcoeff_cancel";
-*)
-
 Goal
   "!!p::('a::ring up). \
 \    [| deg p <= deg r; deg q <= deg r; \
@@ -86,20 +63,20 @@
 (* case "x ~= <0> *)
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (rtac impI 1);
 by (rtac deg_lcoeff_cancel2 1);
   (* replace by linear arithmetic??? *)
   by (rtac le_trans 1);
   by (rtac deg_smult_ring 1);
-  by (simp_tac (simpset() addsplits [expand_if]) 1);
+  by (Simp_tac 1);
   by (Simp_tac 1);
   by (rtac le_trans 1);
   by (rtac deg_mult_ring 1);
   by (rtac le_trans 1);
   by (rtac add_le_mono1 1);
   by (rtac deg_smult_ring 1);
-  by (asm_simp_tac (simpset() addsimps [leI] addsplits [expand_if]) 1);
+  by (asm_simp_tac (simpset() addsimps [leI]) 1);
 by (SELECT_GOAL Auto_tac 1);
 by (Simp_tac 1);
 by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
@@ -155,7 +132,7 @@
 by (rtac disjI2 1);
 by (rtac le_less_trans 1);
 by (rtac deg_smult_ring 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 qed "long_div_unit";
 
 Goal
diff -r b64d86018785 -r 299127ded09d src/HOL/Algebra/poly/UnivPoly.ML
--- a/src/HOL/Algebra/poly/UnivPoly.ML	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.ML	Thu Nov 11 10:25:29 1999 +0100
@@ -212,13 +212,13 @@
 
 Goal "!! a::'a::ring. const (a + b) = const a + const b";
 by (rtac up_eqI 1);
-by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
 qed "const_add";
 
 Goal "!! a::'a::ring. const (a * b) = const a * const b";
 by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
 by (rtac up_eqI 1);
-by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
 qed "const_mult";
 
 Goal "const (<1>::'a::ring) = <1>";
@@ -228,7 +228,7 @@
 
 Goal "const (<0>::'a::ring) = <0>";
 by (rtac up_eqI 1);
-by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
 qed "const_zero";
 
 Addsimps [const_add, const_mult, const_one, const_zero];
diff -r b64d86018785 -r 299127ded09d src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:29 1999 +0100
@@ -17,17 +17,15 @@
   transient :: "'a set => 'a program set"
     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
 
+  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
+    "A ensures B == (A-B co A Un B) Int transient (A-B)"
+
 
 consts
 
-  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
-
   (*LEADS-TO constant for the inductive definition*)
   leads :: "'a program => ('a set * 'a set) set"
 
-  (*visible version of the LEADS-TO relation*)
-  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
-
 
 inductive "leads F"
   intrs 
@@ -44,13 +42,11 @@
   monos Pow_mono
 
 
-  
-defs
-  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
+constdefs
 
-  leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
-
-constdefs
+  (*visible version of the LEADS-TO relation*)
+  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
+    "A leadsTo B == {F. (A,B) : leads F}"
   
   (*wlt F B is the largest set that leads to B*)
   wlt :: "['a program, 'a set] => 'a set"