# HG changeset patch
# User paulson
# Date 1115649536 -7200
# Node ID 9b00875e21f7c650ba6f4f2efa2de9ec5ab634c4
# Parent  dd7b303465a265dcc0ac07a3d177d882f2741e4e
from simplesubst to new subst

diff -r dd7b303465a2 -r 9b00875e21f7 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon May 09 16:38:56 2005 +0200
@@ -357,7 +357,7 @@
       case 0 then show ?case by (simp add: Pi_def)
     next
       case (Suc k) then show ?case
-        by (simplesubst finsum_Suc2) (simp add: Pi_def a_comm)+
+        by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
     qed
   }
   note l = this
diff -r dd7b303465a2 -r 9b00875e21f7 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Mon May 09 16:38:56 2005 +0200
@@ -1,4 +1,4 @@
-(*  Title       : Integration.thy
+(*  ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 2000  University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -262,12 +262,13 @@
  apply (drule partition_rhs)
  apply (drule partition_lhs, auto)
 apply (simp split: nat_diff_split)
-apply (subst partition)
-apply (simplesubst lemma_partition_append2, assumption+)
-   --{*Need to substitute the last occurrence*}
-apply (rule conjI)
-apply (drule_tac [2] lemma_partition_append1)
-apply (auto simp add: partition_lhs partition_rhs)
+apply (subst partition) 
+apply (subst (1 2) lemma_partition_append2, assumption+)
+apply (rule conjI) 
+apply (simp add: partition_lhs)
+apply (drule lemma_partition_append1)
+apply assumption; 
+apply (simp add: partition_rhs)
 done
 
 
diff -r dd7b303465a2 -r 9b00875e21f7 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:38:56 2005 +0200
@@ -1,10 +1,11 @@
-(*  Title       : MacLaurin.thy
+(*  ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 2001 University of Edinburgh
-    Description : MacLaurin series
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
+header{*MacLaurin Series*}
+
 theory MacLaurin
 imports Log
 begin
@@ -583,7 +584,7 @@
       in Maclaurin_all_le_objl)
     apply safe
     apply simp
-    apply (simplesubst mod_Suc_eq_Suc_mod)  --{*simultaneous substitution*}
+    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
     apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
     apply (rule DERIV_minus, simp+)
     apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
diff -r dd7b303465a2 -r 9b00875e21f7 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Induct/LList.thy	Mon May 09 16:38:56 2005 +0200
@@ -865,7 +865,8 @@
        in llist_equalityI)
  apply (rule rangeI)
 apply (safe)
-apply (simplesubst iterates, simp)  --{*two redexes*}
+apply (subst (1 2) iterates)
+apply simp 
 done
 
 subsubsection{* Two proofs that @{text lmap} distributes over lappend *}
diff -r dd7b303465a2 -r 9b00875e21f7 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon May 09 16:38:56 2005 +0200
@@ -134,7 +134,7 @@
 
 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
   apply (induct set: NF)
-  apply (simplesubst app_last)
+  apply (subst app_last)
   apply (rule exI)
   apply (rule conjI)
   apply (rule rtrancl_refl)