# HG changeset patch
# User chaieb
# Date 1187778077 -7200
# Node ID 8d83b1e7c3dd75cea2d6357503b4793ced6f8bbb
# Parent  eaf37b78068321687f3e43c7c7fd957f1dbc9736
Axioms for class no longer use object-universal quantifiers

diff -r eaf37b780683 -r 8d83b1e7c3dd src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Wed Aug 22 02:04:30 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Wed Aug 22 12:21:17 2007 +0200
@@ -212,9 +212,9 @@
 section {* The classical QE after Langford for dense linear orders *}
 
 class dense_linear_order = linorder + 
-  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y" 
-  and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
-  and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+  assumes gt_ex: "\<exists>y. x \<sqsubset> y" 
+  and lt_ex: "\<exists>y. y \<sqsubset> x"
+  and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
 begin
 
 lemma dlo_qe_bnds: 
@@ -306,7 +306,6 @@
 
 interpretation dlo_ordring_class: dense_linear_order ["op \<le> \<Colon> 'a\<Colon>ordered_field \<Rightarrow> _" "op <"]
 apply unfold_locales
-apply auto
 apply (rule_tac x = "x + 1" in exI, simp)
 apply (rule_tac x = "x - 1" in exI, simp)
 apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
@@ -323,10 +322,10 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_ub = linorder +
-  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
+  assumes gt_ex: "\<exists>y. x \<sqsubset> y"
 begin
 
-lemma ge_ex: "\<forall>x. \<exists>y. x \<sqsubseteq> y" using gt_ex by auto
+lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
 
 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
 lemma pinf_conj:
@@ -373,10 +372,10 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_lb = linorder +
-  assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
+  assumes lt_ex: "\<exists>y. y \<sqsubset> x"
 begin
 
-lemma le_ex: "\<forall>x. \<exists>y. y \<sqsubseteq> x" using lt_ex by auto
+lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
 
 
 text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
@@ -422,8 +421,8 @@
 
 class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
-  assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
-     and  between_same: "\<forall>x. between x x = x"
+  assumes between_less: "x \<sqsubset> y \<Longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
+     and  between_same: "between x x = x"
 
 instance advanced constr_dense_linear_order < dense_linear_order
   apply unfold_locales