# 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: "\x. \y. x \ y" - and lt_ex: "\x. \y. y \ x" - and dense: "\x y. x \ y \ (\z. x \ z \ z \ y)" + assumes gt_ex: "\y. x \ y" + and lt_ex: "\y. y \ x" + and dense: "x \ y \ (\z. x \ z \ z \ y)" begin lemma dlo_qe_bnds: @@ -306,7 +306,6 @@ interpretation dlo_ordring_class: dense_linear_order ["op \ \ 'a\ordered_field \ _" "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: "\x. \y. x \ y" + assumes gt_ex: "\y. x \ y" begin -lemma ge_ex: "\x. \y. x \ y" using gt_ex by auto +lemma ge_ex: "\y. x \ y" using gt_ex by auto text {* Theorems for @{text "\z. \x. z \ x \ (P x \ P\<^bsub>+\\<^esub>)"} *} lemma pinf_conj: @@ -373,10 +372,10 @@ text {* Linear order without upper bounds *} class linorder_no_lb = linorder + - assumes lt_ex: "\x. \y. y \ x" + assumes lt_ex: "\y. y \ x" begin -lemma le_ex: "\x. \y. y \ x" using lt_ex by auto +lemma le_ex: "\y. y \ x" using lt_ex by auto text {* Theorems for @{text "\z. \x. x \ z \ (P x \ P\<^bsub>-\\<^esub>)"} *} @@ -422,8 +421,8 @@ class constr_dense_linear_order = linorder_no_lb + linorder_no_ub + fixes between - assumes between_less: "\x y. x \ y \ x \ between x y \ between x y \ y" - and between_same: "\x. between x x = x" + assumes between_less: "x \ y \ x \ between x y \ between x y \ y" + and between_same: "between x x = x" instance advanced constr_dense_linear_order < dense_linear_order apply unfold_locales