src/HOL/UNITY/Follows.thy
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Tue, 05 Jul 2016 13:05:04 +0200 fleury instantiate multiset with multiset ordering
Wed, 25 May 2016 11:50:58 +0200 wenzelm isabelle update_cartouches -c -t;
Fri, 26 Feb 2016 22:44:11 +0100 haftmann more succint formulation of membership for multisets, similar to lists;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Wed, 10 Jun 2015 13:24:16 +0200 Mathias Fleury Renaming multiset operators < ~> <#,...
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 22 Mar 2014 08:37:43 +0100 haftmann generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
Wed, 25 Dec 2013 15:52:25 +0100 haftmann prefer abstract simp rule
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Mon, 22 Feb 2010 09:15:12 +0100 haftmann tuned proofs
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 21 Sep 2009 14:23:04 +0200 haftmann tuned proof; tuned headers
Fri, 08 Dec 2006 18:22:28 +0100 paulson patched up the proofs agsin
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 03 Aug 2004 13:48:00 +0200 paulson new simprules Int_subset_iff and Un_subset_iff
Sat, 08 Feb 2003 16:05:33 +0100 paulson converting HOL/UNITY to use unconditional fairness
Tue, 04 Feb 2003 18:12:40 +0100 paulson some x-symbols
Fri, 31 Jan 2003 20:12:44 +0100 paulson conversion to new-style theories and tidying
Thu, 30 Jan 2003 10:35:56 +0100 paulson converting more UNITY theories to new-style
Wed, 18 Oct 2000 23:42:18 +0200 wenzelm use Multiset from HOL/Library;
Fri, 02 Jun 2000 17:46:16 +0200 paulson new parent MultisetOrder and new results about multiset unions
Wed, 24 May 2000 18:40:01 +0200 paulson restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
Fri, 14 Jan 2000 12:17:53 +0100 paulson still working; a bit of polishing
Thu, 13 Jan 2000 17:30:23 +0100 paulson working version, with Alloc now working on the same state space as the whole
Wed, 22 Dec 1999 17:18:03 +0100 paulson Working version after a FAILED attempt to base Follows upon LeadsETo
Thu, 10 Jun 1999 10:38:11 +0200 paulson shortened Follows to Fols
Mon, 24 May 1999 15:47:06 +0200 paulson Theory of the "Follows" relation
less more (0) tip