# HG changeset patch
# User haftmann
# Date 1217312138 -7200
# Node ID 268a7d02cf7a43f09587d0491b3554ddebe35d0b
# Parent  397de75836a10672894d1e3c43f589a48c1d8b32
declare

diff -r 397de75836a1 -r 268a7d02cf7a src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jul 28 20:49:07 2008 +0200
+++ b/src/HOL/Orderings.thy	Tue Jul 29 08:15:38 2008 +0200
@@ -403,117 +403,80 @@
 (* The type constraint on @{term op =} below is necessary since the operation
    is not a parameter of the locale. *)
 
-lemmas
-  [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] =
-  less_irrefl [THEN notE]
-lemmas
-  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  order_refl
-lemmas
-  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_imp_le
-lemmas
-  [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  antisym
-lemmas
-  [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  eq_refl
-lemmas
-  [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  sym [THEN eq_refl]
-lemmas
-  [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_trans
-lemmas
-  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_le_trans
-lemmas
-  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  le_less_trans
-lemmas
-  [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  order_trans
-lemmas
-  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  le_neq_trans
-lemmas
-  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  neq_le_trans
-lemmas
-  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_imp_neq
-lemmas
-  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-   eq_neq_eq_imp_neq
-lemmas
-  [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_sym
+declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
+  
+declare order_refl  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+  
+declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+  
+declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+  
+declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+  
+declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
 
 end
 
 context linorder
 begin
 
-lemmas
-  [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
+declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
+
+declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
 
-lemmas
-  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_irrefl [THEN notE]
-lemmas
-  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  order_refl
-lemmas
-  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_imp_le
-lemmas
-  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_less [THEN iffD2]
-lemmas
-  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_le [THEN iffD2]
-lemmas
-  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_less [THEN iffD1]
-lemmas
-  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_le [THEN iffD1]
-lemmas
-  [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  antisym
-lemmas
-  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  eq_refl
-lemmas
-  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  sym [THEN eq_refl]
-lemmas
-  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_trans
-lemmas
-  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_le_trans
-lemmas
-  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  le_less_trans
-lemmas
-  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  order_trans
-lemmas
-  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  le_neq_trans
-lemmas
-  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  neq_le_trans
-lemmas
-  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  less_imp_neq
-lemmas
-  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  eq_neq_eq_imp_neq
-lemmas
-  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
-  not_sym
+declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+
+declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
 
 end