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
```