src/HOL/Lattices.thy
changeset 23389 aaca6a8e5414
parent 23087 ad7244663431
child 23878 bd651ecd4b8a
     1.1 --- a/src/HOL/Lattices.thy	Thu Jun 14 18:33:29 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Thu Jun 14 18:33:31 2007 +0200
     1.3 @@ -259,7 +259,7 @@
     1.4    and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
     1.5    shows "x \<sqinter> y = x \<triangle> y"
     1.6  proof (rule antisym)
     1.7 -  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
     1.8 +  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
     1.9  next
    1.10    have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
    1.11    show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
    1.12 @@ -271,7 +271,7 @@
    1.13    and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
    1.14    shows "x \<squnion> y = x \<nabla> y"
    1.15  proof (rule antisym)
    1.16 -  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
    1.17 +  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
    1.18  next
    1.19    have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
    1.20    show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all