# HG changeset patch
# User ballarin
# Date 1078744617 -3600
# Node ID 24724afce166d111e7a907039292a9e1f6ba888a
# Parent  75910c7557c5c3dfbdac66d7caf2ef9cd196af62
Added documentation for transitivity solver setup.

diff -r 75910c7557c5 -r 24724afce166 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 08 11:12:06 2004 +0100
+++ b/src/HOL/HOL.thy	Mon Mar 08 12:16:57 2004 +0100
@@ -954,7 +954,7 @@
   by (rule order_less_asym)
 
 
-subsubsection {* Setup of transitivity reasoner *}
+subsubsection {* Setup of transitivity reasoner as Solver *}
 
 lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
   by (erule contrapos_pn, erule subst, rule order_less_irrefl)
@@ -1015,6 +1015,10 @@
   simpset_of thy
     addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
     addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
+  (* Adding the transitivity reasoners also as safe solvers showed a slight
+     speed up, but the reasoning strength appears to be not higher (at least
+     no breaking of additional proofs in the entire HOL distribution, as
+     of 5 March 2004, was observed). *)
   thy))
 *}
 
@@ -1028,6 +1032,10 @@
   {* simple transitivity reasoner *}
 *)
 
+(*
+declare order.order_refl [simp del] order_less_irrefl [simp del]
+*)
+
 subsubsection "Bounded quantifiers"
 
 syntax