src/HOL/Wellfounded.thy
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Fri, 11 Jun 2010 17:14:02 +0200 haftmann declare lex_prod_def [code del]
Wed, 05 May 2010 00:59:59 +0200 krauss repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Thu, 11 Mar 2010 14:40:29 +0100 haftmann Big_Operators now in Main rather than Plain
Wed, 10 Mar 2010 16:53:27 +0100 haftmann split off theory Big_Operators from theory Finite_Set
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Mon, 26 Oct 2009 23:27:16 +0100 krauss authentic constants; moved "acyclic" further down
Mon, 26 Oct 2009 23:26:57 +0100 krauss point-free characterization of well-foundedness
Mon, 26 Oct 2009 23:26:18 +0100 krauss replaced (outdated) comments by explicit statements
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 23 Sep 2009 16:32:53 +0200 haftmann simplified proof
Mon, 31 Aug 2009 20:34:48 +0200 krauss moved lemma Wellfounded.in_inv_image to Relation.thy
Mon, 31 Aug 2009 20:34:44 +0200 krauss moved wfrec to Recdef.thy
Mon, 31 Aug 2009 20:32:00 +0200 krauss no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
Tue, 28 Jul 2009 13:37:08 +0200 haftmann explicit is better than implicit
Tue, 28 Jul 2009 08:48:56 +0200 krauss moved obsolete same_fst to Recdef.thy
Mon, 27 Jul 2009 21:47:41 +0200 krauss "more standard" argument order of relation composition (op O)
Sat, 25 Jul 2009 18:44:55 +0200 haftmann explicit is better than implicit
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
Sun, 26 Apr 2009 20:23:09 +0200 haftmann reverted slip in theory imports
Sun, 26 Apr 2009 08:34:53 +0200 haftmann adjusted to changes in power syntax
Wed, 11 Mar 2009 08:45:47 +0100 haftmann explicit code equations for some rarely used pred operations
Wed, 21 Jan 2009 23:40:23 +0100 haftmann changed import hierarchy
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID
Tue, 16 Dec 2008 08:46:07 +0100 krauss method "sizechange" proves termination of functions; added more infrastructure for termination proofs
Tue, 18 Nov 2008 21:17:14 +0100 krauss removed lemmas called lemma1 and lemma2
Wed, 12 Nov 2008 17:23:22 +0100 krauss min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Wed, 17 Sep 2008 15:59:23 +0200 krauss wf_finite_psubset[simp], in_finite_psubset[simp]
Mon, 11 Aug 2008 14:49:53 +0200 haftmann moved class wellorder to theory Orderings
Fri, 23 May 2008 17:19:24 +0200 krauss rearranged subsections
Wed, 07 May 2008 10:56:52 +0200 berghofe - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
less more (0) tip