src/HOL/Wellfounded.thy
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Sun, 27 Dec 2015 22:07:17 +0100 wenzelm discontinued ASCII replacement syntax <*>;
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 17 Jun 2015 14:35:50 +0100 paulson New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
Mon, 27 Apr 2015 15:02:51 +0200 nipkow new lemma
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries;
Wed, 23 Apr 2014 10:23:27 +0200 blanchet move size hooks together, with new one preceding old one and sharing same theory data
Thu, 03 Apr 2014 10:51:22 +0200 blanchet use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod'
Fri, 17 Jan 2014 10:02:50 +0100 blanchet folded 'Wellfounded_More_FP' into 'Wellfounded'
Sun, 10 Nov 2013 15:05:06 +0100 haftmann qualifed popular user space names
Sat, 20 Oct 2012 09:09:34 +0200 bulwahn adjusting proofs
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Mon, 12 Mar 2012 15:12:22 +0100 noschinl tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Mon, 30 Jan 2012 13:55:19 +0100 bulwahn adding code_unfold to make measure executable
Sat, 28 Jan 2012 06:13:03 +0100 bulwahn reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
Wed, 25 Jan 2012 16:07:48 +0100 bulwahn adding very basic code generation to Wellfounded theory
Tue, 10 Jan 2012 18:12:55 +0100 berghofe pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Thu, 13 Oct 2011 23:02:59 +0200 haftmann moved acyclic predicate up in hierarchy
Thu, 13 Oct 2011 22:56:19 +0200 haftmann modernized definitions
Tue, 20 Sep 2011 21:47:52 +0200 haftmann tuned specification and lemma distribution among theories; tuned proofs
Thu, 15 Sep 2011 12:40:08 -0400 hoelzl removed further legacy rules from Complete_Lattices
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Thu, 11 Aug 2011 09:15:45 +0200 krauss removed unused material, which does not really belong here
Wed, 01 Jun 2011 15:53:47 +0200 nipkow tuned lemmas
Wed, 01 Jun 2011 11:51:25 +0200 nipkow new lemmas
Tue, 08 Feb 2011 07:42:08 +0100 nipkow added termination lemmas
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Thu, 18 Nov 2010 17:01:16 +0100 haftmann map_pair replaces prod_fun
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
less more (0) -60 tip