# 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