src/HOL/HOL.thy
changeset 14444 24724afce166
parent 14430 5cb24165a2e1
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/HOL.thy	Mon Mar 08 11:12:06 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Mar 08 12:16:57 2004 +0100
     1.3 @@ -954,7 +954,7 @@
     1.4    by (rule order_less_asym)
     1.5  
     1.6  
     1.7 -subsubsection {* Setup of transitivity reasoner *}
     1.8 +subsubsection {* Setup of transitivity reasoner as Solver *}
     1.9  
    1.10  lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
    1.11    by (erule contrapos_pn, erule subst, rule order_less_irrefl)
    1.12 @@ -1015,6 +1015,10 @@
    1.13    simpset_of thy
    1.14      addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
    1.15      addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
    1.16 +  (* Adding the transitivity reasoners also as safe solvers showed a slight
    1.17 +     speed up, but the reasoning strength appears to be not higher (at least
    1.18 +     no breaking of additional proofs in the entire HOL distribution, as
    1.19 +     of 5 March 2004, was observed). *)
    1.20    thy))
    1.21  *}
    1.22  
    1.23 @@ -1028,6 +1032,10 @@
    1.24    {* simple transitivity reasoner *}
    1.25  *)
    1.26  
    1.27 +(*
    1.28 +declare order.order_refl [simp del] order_less_irrefl [simp del]
    1.29 +*)
    1.30 +
    1.31  subsubsection "Bounded quantifiers"
    1.32  
    1.33  syntax