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