src/HOL/Relation.thy
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Wed, 11 Feb 2015 14:07:28 +0100 Andreas Lochbihler add lemma
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Thu, 29 May 2014 11:11:22 +0200 nipkow typo
Tue, 29 Apr 2014 16:02:02 +0200 wenzelm prefer plain ASCII / latex over not-so-universal Unicode;
Sat, 26 Apr 2014 14:53:22 +0200 haftmann more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
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
Thu, 13 Mar 2014 13:18:13 +0100 blanchet killed a few 'metis' calls
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Tue, 21 Jan 2014 13:21:55 +0100 traytel removed theory dependency of BNF_LFP on Datatype
less more (0) -100 -15 tip