# HG changeset patch
# User ballarin
# Date 1111678455 -3600
# Node ID 4723248c982b5e073e09b0dec7df730820e2b061
# Parent  4c964b85df5ca84221c15ede5a8fb1c270c02466
Transitivity reasoner ignores types amenable to linear arithmetic.
These are currently nat, int, real.

Fixed IsaMakefile.

diff -r 4c964b85df5c -r 4723248c982b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 24 10:59:21 2005 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 24 16:34:15 2005 +0100
@@ -96,7 +96,8 @@
   Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
   Refute.thy ROOT.ML \
   Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
-  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
+  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \
+  Orderings.ML Orderings.thy Ring_and_Field.thy\
   Set.ML Set.thy SetInterval.thy \
   Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
   Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
diff -r 4c964b85df5c -r 4723248c982b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Mar 24 10:59:21 2005 +0100
+++ b/src/HOL/Orderings.thy	Thu Mar 24 16:34:15 2005 +0100
@@ -287,7 +287,10 @@
    Quasi_Tac.quasi_tac are not of much use. *)
 
 fun decomp_gen sort sign (Trueprop $ t) =
-  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
+  let fun of_sort t = let val T = type_of t in
+        (* exclude numeric types: linear arithmetic subsumes transitivity *)
+        T <> HOLogic.natT andalso T <> HOLogic.intT andalso
+        T <> HOLogic.realT andalso Sign.of_sort sign (T, sort) end
   fun dec (Const ("Not", _) $ t) = (
 	  case dec t of
 	    NONE => NONE