# HG changeset patch
# User haftmann
# Date 1196236900 -3600
# Node ID 4c98517601ceb14f62e4398bd80845acf4b36fe3
# Parent  65de74f62874c47ffcdb5d65cbe902715cedd6ca
dropped dead code

diff -r 65de74f62874 -r 4c98517601ce src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Nov 28 09:01:39 2007 +0100
+++ b/src/HOL/arith_data.ML	Wed Nov 28 09:01:40 2007 +0100
@@ -163,52 +163,6 @@
 val arith_data_setup =
   Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
 
-
-(* FIXME dead code *)
-(* antisymmetry:
-   combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
-
-local
-val antisym = mk_meta_eq order_antisym
-val not_lessD = @{thm linorder_not_less} RS iffD1
-fun prp t thm = (#prop(rep_thm thm) = t)
-in
-fun antisym_eq prems thm =
-  let
-    val r = #prop(rep_thm thm);
-  in
-    case r of
-      Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
-        let val r' = Tr $ (c $ t $ s)
-        in
-          case Library.find_first (prp r') prems of
-            NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
-              in case Library.find_first (prp r') prems of
-                   NONE => []
-                 | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
-              end
-          | SOME thm' => [thm' RS (thm RS antisym)]
-        end
-    | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
-        let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
-        in
-          case Library.find_first (prp r') prems of
-            NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
-              in case Library.find_first (prp r') prems of
-                   NONE => []
-                 | SOME thm' =>
-                     [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
-              end
-          | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
-        end
-    | _ => []
-  end
-  handle THM _ => []
-end;
-*)
-
 end;
 
 open ArithData;