--- 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
--- 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"
--- 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"
--- 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)
--- 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 .
--- 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"
--- 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)
--- 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)
--- 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
--- 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
--- 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':
--- 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
--- 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)
--- 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
--- 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
--- 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