src/HOL/Transitive_Closure.thy
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2007-01-24 paulson 2007-01-24 some new lemmas
2007-01-17 paulson 2007-01-17 induction rules for trancl/rtrancl expressed using subsets
2006-11-29 wenzelm 2006-11-29 simplified method setup; reactivated dead code;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-26 krauss 2006-09-26 Changed precedence of "op O" (relation composition) from 60 to 75.
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-03-10 huffman 2006-03-10 added many simple lemmas
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-06-21 kleing 2005-06-21 lemma, equation between rtrancl and trancl
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-02-28 paulson 2005-02-28 unfold theorems for trancl and rtrancl
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
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 ***