src/HOL/Transitive_Closure.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-02 ballarin 2004-08-02 Documentation added; minor improvements.
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-02-21 nipkow 2004-02-21 Transitive_Closure: added consumes and case_names attributes Isar: fixed parameter name handling in simulatneous induction which I had not done properly 2 years ago.
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2004-01-05 nipkow 2004-01-05 undid split_comp_eq[simp] because it leads to nontermination together with split_def!
2003-09-26 paulson 2003-09-26 misc tidying
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
2002-11-27 berghofe 2002-11-27 Replaced some blasts by rules.
2002-11-13 berghofe 2002-11-13 Transitive closure is now defined inductively as well.
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-01-21 berghofe 2002-01-21 Made some proofs constructive.
2002-01-09 wenzelm 2002-01-09 converted theory Transitive_Closure;
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-09 kleing 2001-12-09 setup [trans] rules for calculational Isar reasoning
2001-05-22 berghofe 2001-05-22 Transitive closure is now defined via "inductive".
2001-02-14 paulson 2001-02-14 a new theorem from Bryan Ford
2001-02-09 wenzelm 2001-02-09 tuned;
2001-02-09 wenzelm 2001-02-09 unsymbolized; tuned;
2001-01-29 nipkow 2001-01-29 Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
2001-01-26 wenzelm 2001-01-26 Transitive_Closure turned into new-style theory;
2001-01-09 wenzelm 2001-01-09 syntax (xsymbols);
2000-12-01 wenzelm 2000-12-01 superscripts: syntax (latex);
2000-10-25 wenzelm 2000-10-25 more "xsymbols" syntax;
2000-10-12 nipkow 2000-10-12 *** empty log message ***