summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | ballarin |

Mon, 08 Mar 2004 12:16:57 +0100 | |

changeset 14444 | 24724afce166 |

parent 14443 | 75910c7557c5 |

child 14445 | 4392cb82018b |

Added documentation for transitivity solver setup.

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |

--- 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