src/ZF/ex/Limit.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
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";
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 20 Aug 2009 15:23:25 +0200 paulson A few Isar scripts
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Thu, 28 Aug 2003 01:56:40 +0200 skalberg Extended the notion of letter and digit, such that now one may use greek,
Tue, 27 May 2003 11:39:03 +0200 paulson updating ZF-UNITY with Sidi's new material
Tue, 01 Oct 2002 13:26:10 +0200 paulson Numerous cosmetic changes, prompted by the new simplifier
Mon, 30 Sep 2002 16:48:15 +0200 berghofe Adapted to new simplifier.
Tue, 27 Aug 2002 11:09:35 +0200 wenzelm *** empty log message ***
Wed, 10 Jul 2002 16:54:07 +0200 paulson Fixed quantified variable name preservation for ball and bex (bounded quants)
Fri, 24 May 2002 13:15:37 +0200 paulson conversion of Perm to Isar. Strengthening of comp_fun_apply
Thu, 23 May 2002 17:05:21 +0200 paulson new definition of "apply" and new simprule "beta_if"
Fri, 10 May 2002 10:22:45 +0200 paulson tidied
Mon, 15 Apr 2002 10:18:01 +0200 paulson converted theory ex/Limit to Isar script, but it still needs work!
Mon, 21 May 2001 14:36:24 +0200 paulson X-symbols for set theory
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Tue, 06 Feb 1996 12:27:17 +0100 clasohm expanded tabs
Sat, 09 Dec 1995 13:36:11 +0100 clasohm removed quotes from consts and syntax sections
Mon, 16 Oct 1995 14:56:24 +0100 paulson The inverse limit construction -- thanks to Sten Agerholm
less more (0) tip