# HG changeset patch
# User wenzelm
# Date 1181855079 -7200
# Node ID 474ff28210c0e59adf8ecbbd2b636509a2f0fcdf
# Parent  31781b2de73da5176096b5c20cca6d852e5d6eaf
tuned proofs;

diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Char_nat.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -13,7 +13,7 @@
 
 fun
   nat_of_nibble :: "nibble \<Rightarrow> nat" where
-  "nat_of_nibble Nibble0 = 0"
+    "nat_of_nibble Nibble0 = 0"
   | "nat_of_nibble Nibble1 = 1"
   | "nat_of_nibble Nibble2 = 2"
   | "nat_of_nibble Nibble3 = 3"
@@ -83,7 +83,8 @@
 
 lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
 proof -
-  have nibble_nat_enum: "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
+  have nibble_nat_enum:
+    "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
   proof -
     have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
     have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
@@ -111,8 +112,7 @@
 text {* Conversion between chars and nats. *}
 
 definition
-  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble"
-where
+  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
 
 lemma nibble_of_pair [code func]:
@@ -146,7 +146,7 @@
   proof -
     fix m k n :: nat
     show "(k * n + m) mod n = m mod n"
-    by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
+      by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
   qed
   from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
     and k: "k = n div 256" and l: "l = n mod 256" by blast
@@ -163,28 +163,31 @@
   have aux4: "(k * 256 + l) mod 16 = l mod 16"
     unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
   show ?thesis
-  by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair nat_of_nibble_of_nat mod_mult_distrib
-    n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
+    by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
+      nat_of_nibble_of_nat mod_mult_distrib
+      n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
 qed
 
 lemma nibble_pair_of_nat_char:
   "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
 proof -
   have nat_of_nibble_256:
-    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 = nat_of_nibble n * 16 + nat_of_nibble m"
+    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
+      nat_of_nibble n * 16 + nat_of_nibble m"
   proof -
     fix n m
     have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
-    using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
-    have less_eq_240: "nat_of_nibble n * 16 \<le> 240" using nat_of_nibble_less_eq_15 by auto
+      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
+    have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
+      using nat_of_nibble_less_eq_15 by auto
     have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
-    by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
+      by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
     then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
     then show "?rhs mod 256 = ?rhs" by auto
   qed
   show ?thesis
-  unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
-  by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
+    unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
+    by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
 qed
 
 
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Char_ord.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -13,32 +13,36 @@
   nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
   nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
 proof
-  fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
+  fix n :: nibble
+  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
 next
   fix n m q :: nibble
   assume "n \<le> m"
-  and "m \<le> q"
+    and "m \<le> q"
   then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
 next
   fix n m :: nibble
   assume "n \<le> m"
-  and "m \<le> n"
-  then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq)
+    and "m \<le> n"
+  then show "n = m"
+    unfolding nibble_less_eq_def nibble_less_def
+    by (auto simp add: nat_of_nibble_eq)
 next
   fix n m :: nibble
   show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
-  unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq)
+    unfolding nibble_less_eq_def nibble_less_def less_le
+    by (auto simp add: nat_of_nibble_eq)
 next
   fix n m :: nibble
   show "n \<le> m \<or> m \<le> n"
-  unfolding nibble_less_eq_def by auto
+    unfolding nibble_less_eq_def by auto
 qed
 
 instance nibble :: distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
-  by default
-    (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+    "inf \<equiv> min"
+    "sup \<equiv> max"
+  by default (auto simp add:
+    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
 
 instance char :: linorder
   char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
@@ -50,10 +54,10 @@
 lemmas [code func del] = char_less_eq_def char_less_def
 
 instance char :: distrib_lattice
-  "inf \<equiv> min"
-  "sup \<equiv> max"
-  by default
-    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
+    "inf \<equiv> min"
+    "sup \<equiv> max"
+  by default (auto simp add:
+    inf_char_def sup_char_def min_max.sup_inf_distrib1)
 
 lemma [simp, code func]:
   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -48,13 +48,13 @@
   fixes k
   assumes "k \<ge> 0"
   shows "number_of k = nat_of_int (number_of k)"
-  unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
+  unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
 
 lemma nat_of_int_of_number_of_aux:
   fixes k
   assumes "Numeral.Pls \<le> k \<equiv> True"
   shows "k \<ge> 0"
-  using prems unfolding Pls_def by simp
+  using assms unfolding Pls_def by simp
 
 lemma nat_of_int_int:
   "nat_of_int (int' n) = n"
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -56,10 +56,9 @@
   insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insertl x xs = (if member xs x then xs else x#xs)"
 
-lemma
-  [code target: List]: "member [] y \<longleftrightarrow> False"
+lemma [code target: List]: "member [] y \<longleftrightarrow> False"
   and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
-unfolding member_def by (induct xs) simp_all
+  unfolding member_def by (induct xs) simp_all
 
 fun
   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -201,7 +200,7 @@
   fixes ys
   assumes distnct: "distinct ys"
   shows "set (subtract' ys xs) = set ys - set xs"
-  and "distinct (subtract' ys xs)"
+    and "distinct (subtract' ys xs)"
   unfolding subtract'_def flip_def subtract_def
   using distnct by (induct xs arbitrary: ys) auto
 
@@ -211,7 +210,8 @@
 
 lemma iso_unions:
   "set (unions xss) = \<Union> set (map set xss)"
-unfolding unions_def proof (induct xss)
+  unfolding unions_def
+proof (induct xss)
   case Nil show ?case by simp
 next
   case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -399,7 +399,7 @@
     hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
       by (simp add: mod_Suc)
     also from fst_p0 have "\<dots> = fst p" .
-    also have "\<dots> = end_node p" by assumption
+    also have "\<dots> = end_node p" by fact
     also have "\<dots> = snd (snd (path_nth p ?k))" 
       by (auto simp: endnode_nth wrap)
     finally show ?thesis .
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -346,7 +346,7 @@
 lemma inf_img_fin_domE:
   assumes "finite (f`A)" and "infinite A"
   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
-  using prems by (blast dest: inf_img_fin_dom)
+  using assms by (blast dest: inf_img_fin_dom)
 
 
 subsection "Infinitely Many and Almost All"
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Kleene_Algebras.thy
--- a/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -100,8 +100,7 @@
   fixes l :: "'a :: complete_lattice"
   assumes "l \<le> M i"
   shows "l \<le> (SUP i. M i)"
-  using prems
-  by (rule order_trans) (rule le_SUPI [OF UNIV_I])
+  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
 
 lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
   unfolding order_def by simp
@@ -428,7 +427,7 @@
   fixes A X :: "'a :: {kleene}"
   assumes "mk_tcl_dom (A, X)"
   shows "mk_tcl A X = X * star A"
-  using prems
+  using assms
   by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
 
 lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
@@ -446,7 +445,7 @@
   fixes A X :: "'a :: {kleene}"
   assumes "mk_tcl A A \<noteq> 0"
   shows "mk_tcl A A = tcl A"
-  using prems mk_tcl_default mk_tcl_correctness
+  using assms mk_tcl_default mk_tcl_correctness
   unfolding tcl_def 
   by (auto simp:star_commute)
 
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -26,7 +26,7 @@
 lemma prefixE [elim?]:
   assumes "xs \<le> ys"
   obtains zs where "ys = xs @ zs"
-  using prems unfolding prefix_def by blast
+  using assms unfolding prefix_def by blast
 
 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
   unfolding strict_prefix_def prefix_def by blast
@@ -47,7 +47,7 @@
   fixes xs ys :: "'a list"
   assumes "xs < ys"
   obtains "xs \<le> ys" and "xs \<noteq> ys"
-  using prems unfolding strict_prefix_def by blast
+  using assms unfolding strict_prefix_def by blast
 
 
 subsection {* Basic properties of prefixes *}
@@ -168,7 +168,7 @@
 lemma parallelE [elim]:
   assumes "xs \<parallel> ys"
   obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
-  using prems unfolding parallel_def by blast
+  using assms unfolding parallel_def by blast
 
 theorem prefix_cases:
   obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
@@ -227,7 +227,7 @@
 lemma postfixE [elim?]:
   assumes "xs >>= ys"
   obtains zs where "xs = zs @ ys"
-  using prems unfolding postfix_def by blast
+  using assms unfolding postfix_def by blast
 
 lemma postfix_refl [iff]: "xs >>= xs"
   by (auto simp add: postfix_def)
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/NatPair.thy
--- a/src/HOL/Library/NatPair.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/NatPair.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -73,22 +73,19 @@
 theorem nat2_to_nat_inj: "inj nat2_to_nat"
 proof -
   {
-    fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
+    fix u v x y
+    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
     then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
-    also from prems [symmetric] have "x+y \<le> u+v"
+    also from eq1 [symmetric] have "x+y \<le> u+v"
       by (rule nat2_to_nat_help)
-    finally have eq: "u+v = x+y" .
-    with prems have ux: "u=x"
+    finally have eq2: "u+v = x+y" .
+    with eq1 have ux: "u=x"
       by (simp add: nat2_to_nat_def Let_def)
-    with eq have vy: "v=y"
-      by simp
-    with ux have "(u,v) = (x,y)"
-      by simp
+    with eq2 have vy: "v=y" by simp
+    with ux have "(u,v) = (x,y)" by simp
   }
-  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
-    by fast
-  then show ?thesis
-    by (unfold inj_on_def) simp
+  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
+  then show ?thesis unfolding inj_on_def by simp
 qed
 
 end
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -103,7 +103,7 @@
 theorem lookup_append_none:
   assumes "lookup env xs = None"
   shows "lookup env (xs @ ys) = None"
-  using prems
+  using assms
 proof (induct xs arbitrary: env)
   case Nil
   then have False by simp
@@ -140,7 +140,7 @@
 theorem lookup_append_some:
   assumes "lookup env xs = Some e"
   shows "lookup env (xs @ ys) = lookup e ys"
-  using prems
+  using assms
 proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
@@ -190,7 +190,7 @@
   assumes "lookup env (xs @ ys) = Some e"
   shows "\<exists>e. lookup env xs = Some e"
 proof -
-  from prems have "lookup env (xs @ ys) \<noteq> None" by simp
+  from assms have "lookup env (xs @ ys) \<noteq> None" by simp
   then have "lookup env xs \<noteq> None"
     by (rule contrapos_nn) (simp only: lookup_append_none)
   then show ?thesis by (simp)
@@ -208,7 +208,7 @@
     lookup env xs = Some (Env b' es') \<and>
     es' y = Some env' \<and>
     lookup env' ys = Some e"
-  using prems
+  using assms
 proof (induct xs arbitrary: env e)
   case Nil
   from Nil.prems have "lookup env (y # ys) = Some e"
@@ -328,7 +328,7 @@
 theorem lookup_update_some:
   assumes "lookup env xs = Some e"
   shows "lookup (update xs (Some env') env) xs = Some env'"
-  using prems
+  using assms
 proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
@@ -377,7 +377,7 @@
 theorem update_append_none:
   assumes "lookup env xs = None"
   shows "update (xs @ y # ys) opt env = env"
-  using prems
+  using assms
 proof (induct xs arbitrary: env)
   case Nil
   then have False by simp
@@ -420,7 +420,7 @@
 theorem update_append_some:
   assumes "lookup env xs = Some e"
   shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
-  using prems
+  using assms
 proof (induct xs arbitrary: env e)
   case Nil
   then have "env = e" by simp
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -185,7 +185,7 @@
   assumes "!!X Y. f X Y == g (pick X) (pick Y)"
     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-  using prems and TrueI
+  using assms and TrueI
   by (rule quot_cond_function)
 
 theorem quot_function':
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/SCT_Implementation.thy
--- a/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -88,9 +88,9 @@
   assumes "A \<le> B"
   assumes "no_bad_graphs B"
   shows "no_bad_graphs A"
-using prems
-unfolding no_bad_graphs_def has_edge_def graph_leq_def 
-by blast
+  using assms
+  unfolding no_bad_graphs_def has_edge_def graph_leq_def 
+  by blast
 
 
 
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/SCT_Interpretation.thy
--- a/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -74,7 +74,7 @@
 lemma some_rd:
   assumes "mk_rel rds x y"
   shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
-  using prems
+  using assms
   by (induct rds) (auto simp:in_cdesc_def)
 
 (* from a value sequence, get a sequence of rds *)
@@ -125,19 +125,19 @@
 
 
 lemma decr_in_cdesc:
-  assumes	"in_cdesc RD1 y x"
+  assumes "in_cdesc RD1 y x"
   assumes "in_cdesc RD2 z y"
   assumes "decr RD1 RD2 m1 m2"
   shows "m2 y < m1 x"
-  using prems
+  using assms
   by (cases RD1, cases RD2, auto simp:decr_def)
 
 lemma decreq_in_cdesc:
-  assumes	"in_cdesc RD1 y x"
+  assumes "in_cdesc RD1 y x"
   assumes "in_cdesc RD2 z y"
   assumes "decreq RD1 RD2 m1 m2"
   shows "m2 y \<le> m1 x"
-  using prems
+  using assms
   by (cases RD1, cases RD2, auto simp:decreq_def)
 
 
@@ -208,7 +208,7 @@
   assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
   assumes "approx (Graph Es) c1 c2 ms1 ms2"
   shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
-  using prems
+  using assms
   unfolding approx_def has_edge_def dest_graph.simps decr_def
   by auto
 
@@ -216,7 +216,7 @@
   assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
   assumes "approx (Graph Es) c1 c2 ms1 ms2"
   shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
-  using prems
+  using assms
   unfolding approx_def has_edge_def dest_graph.simps decreq_def
   by auto
 
@@ -276,7 +276,7 @@
   assumes "in_cdesc RD1 y x"
   assumes "in_cdesc RD2 z y"
   shows "\<not> no_step RD1 RD2"
-  using prems
+  using assms
   by (cases RD1, cases RD2) (auto simp:no_step_def)
 
 
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/SCT_Misc.thy
--- a/src/HOL/Library/SCT_Misc.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/SCT_Misc.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -32,7 +32,7 @@
   assumes "a3 \<Longrightarrow> thesis"
   assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   shows "thesis"
-  using prems
+  using assms
   by auto
 
 
@@ -44,32 +44,34 @@
 
 subsubsection {* Increasing sequences *}
 
-definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
-where
+definition
+  increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
   "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
 
 lemma increasing_strict:
   assumes "increasing s"
   assumes "i < j"
   shows "s i < s j"
-  using prems
+  using assms
   unfolding increasing_def by simp
 
 lemma increasing_weak:
   assumes "increasing s"
   assumes "i \<le> j"
   shows "s i \<le> s j"
-  using prems increasing_strict[of s i j]
-  by (cases "i<j") auto
+  using assms increasing_strict[of s i j]
+  by (cases "i < j") auto
 
 lemma increasing_inc:
-  assumes [simp]: "increasing s"
+  assumes "increasing s"
   shows "n \<le> s n"
 proof (induct n)
+  case 0 then show ?case by simp
+next
   case (Suc n)
-  with increasing_strict[of s n "Suc n"]
+  with increasing_strict [OF `increasing s`, of n "Suc n"]
   show ?case by auto
-qed auto
+qed
 
 lemma increasing_bij:
   assumes [simp]: "increasing s"
@@ -162,10 +164,10 @@
 qed 
   
 lemma in_section_of: 
-  assumes [simp, intro]: "increasing s"
+  assumes "increasing s"
   assumes "s i \<le> k"
   shows "k \<in> section s (section_of s k)"
-  using prems
+  using assms
   by (auto intro:section_of1 section_of2)
 
 end
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -797,7 +797,7 @@
 
     have "i < s (Suc ?k)" by (rule section_of2) simp
     also have "\<dots> \<le> s j"
-      by (rule increasing_weak [of s], assumption) (insert `?k < j`, arith)
+      by (rule increasing_weak [OF `increasing s`]) (insert `?k < j`, arith)
     also note `\<dots> \<le> l`
     finally have "i < l" .
     with desc
diff -r 31781b2de73d -r 474ff28210c0 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -591,7 +591,7 @@
   assumes "root =xs\<Rightarrow> root'"
     and "\<exists>att dir. root = Env att dir"
   shows "\<exists>att dir. root' = Env att dir"
-  using transition_type_safe and prems
+  using transition_type_safe and assms
 proof (rule transitions_invariant)
   show "\<forall>x \<in> set xs. True" by blast
 qed