src/HOL/Decision_Procs/Dense_Linear_Order.thy
changeset 54868 bab6cade3cc5
parent 53215 5e47c31c6f7c
child 55792 687240115804
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Dec 26 22:47:49 2013 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Dec 27 14:35:14 2013 +0100
     1.3 @@ -452,8 +452,9 @@
     1.4    fixes between
     1.5    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
     1.6      and between_same: "between x x = x"
     1.7 +begin
     1.8  
     1.9 -sublocale  constr_dense_linorder < dlo: unbounded_dense_linorder 
    1.10 +sublocale dlo: unbounded_dense_linorder 
    1.11    apply unfold_locales
    1.12    using gt_ex lt_ex between_less
    1.13    apply auto
    1.14 @@ -461,9 +462,6 @@
    1.15    apply simp
    1.16    done
    1.17  
    1.18 -context constr_dense_linorder
    1.19 -begin
    1.20 -
    1.21  lemma rinf_U[no_atp]:
    1.22    assumes fU: "finite U"
    1.23      and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x