src/ZF/Induct/Multiset.thy
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Mon, 23 Mar 2015 21:05:17 +0100 wenzelm prefer local fixes;
Thu, 11 Sep 2014 21:11:03 +0200 blanchet fixed some spelling mistakes
Wed, 11 Jun 2014 14:24:23 +1000 Thomas Sewell Hypsubst preserves equality hypotheses
Thu, 15 Mar 2012 16:35:02 +0000 paulson replacing ":" by "\<in>"
Tue, 06 Mar 2012 16:46:27 +0000 paulson mathematical symbols for Isabelle/ZF example theories
Sun, 20 Nov 2011 20:15:02 +0100 wenzelm eliminated obsolete "standard";
Thu, 11 Feb 2010 22:06:37 +0100 wenzelm numeral syntax: clarify parse trees vs. actual terms;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 26 Mar 2008 22:40:09 +0100 wenzelm rule swap: renamed Pa to P;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Sun, 07 Oct 2007 15:49:25 +0200 wenzelm replaced some 'translations' by 'abbreviation';
Mon, 09 Oct 2006 02:19:51 +0200 wenzelm attribute symmetric: zero_var_indexes;
Thu, 15 Dec 2005 19:42:03 +0100 wenzelm improved proofs;
Mon, 01 Aug 2005 19:20:26 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Fri, 17 Sep 2004 16:08:52 +0200 paulson converted ZF/Induct/Multiset to Isar script
Tue, 27 May 2003 11:39:03 +0200 paulson updating ZF-UNITY with Sidi's new material
Fri, 15 Feb 2002 12:07:27 +0100 paulson a new definition of "restrict"
Wed, 30 Jan 2002 12:22:40 +0100 paulson Multiset: added the translation Mult(A) => A-||>nat-{0}
Sat, 29 Dec 2001 18:36:12 +0100 wenzelm tuned document sources;
Wed, 07 Nov 2001 18:12:12 +0100 paulson Sidi Ehmety's port of the fold_set operator and multisets to ZF.
less more (0) tip