src/HOL/Library/Kleene_Algebras.thy
 changeset 23394 474ff28210c0 parent 22665 cf152ff55d16 child 23416 b73a6b72f706
```     1.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:36 2007 +0200
1.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Thu Jun 14 23:04:39 2007 +0200
1.3 @@ -100,8 +100,7 @@
1.4    fixes l :: "'a :: complete_lattice"
1.5    assumes "l \<le> M i"
1.6    shows "l \<le> (SUP i. M i)"
1.7 -  using prems
1.8 -  by (rule order_trans) (rule le_SUPI [OF UNIV_I])
1.9 +  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
1.10
1.11  lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
1.12    unfolding order_def by simp
1.13 @@ -428,7 +427,7 @@
1.14    fixes A X :: "'a :: {kleene}"
1.15    assumes "mk_tcl_dom (A, X)"
1.16    shows "mk_tcl A X = X * star A"
1.17 -  using prems
1.18 +  using assms
1.19    by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
1.20
1.21  lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
1.22 @@ -446,7 +445,7 @@
1.23    fixes A X :: "'a :: {kleene}"
1.24    assumes "mk_tcl A A \<noteq> 0"
1.25    shows "mk_tcl A A = tcl A"
1.26 -  using prems mk_tcl_default mk_tcl_correctness
1.27 +  using assms mk_tcl_default mk_tcl_correctness
1.28    unfolding tcl_def
1.29    by (auto simp:star_commute)
1.30
```