summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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