src/HOLCF/ex/Stream.thy
Tue, 02 Mar 2010 17:20:03 -0800 huffman variable name changed
Tue, 02 Mar 2010 04:31:50 -0800 huffman re-enable bisim code, now in domain_theorems.ML
Tue, 02 Mar 2010 00:34:26 -0800 huffman domain package no longer generates copy functions; all proofs use take functions instead
Wed, 24 Feb 2010 16:15:03 -0800 huffman reorganizing domain package code (in progress)
Wed, 24 Feb 2010 14:20:07 -0800 huffman change domain package's treatment of variable names in theorems to be like datatype package
Thu, 18 Feb 2010 13:29:59 -0800 huffman get rid of warnings about duplicate simp rules in all HOLCF theories
Wed, 17 Feb 2010 10:00:22 -0800 huffman remove $ from all HOLCF files
Wed, 17 Feb 2010 09:08:58 -0800 huffman fix warnings about duplicate simp rules
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Sun, 10 May 2009 14:21:41 +0200 nipkow fixed HOLCF proofs
Mon, 13 Apr 2009 09:29:55 -0700 huffman domain package now generates iff rules for definedness of constructors
Mon, 30 Mar 2009 13:55:05 -0700 huffman domain package declares more simp rules
Tue, 10 Feb 2009 10:25:09 +0000 paulson Repaired a proof that did, after all, refer to the theorem nat_induct2.
Wed, 14 Jan 2009 17:11:29 -0800 huffman change to simpler, more extensible continuity simproc
Wed, 25 Jun 2008 21:25:51 +0200 wenzelm modernized specifications;
Tue, 10 Jun 2008 15:31:03 +0200 haftmann adjusted some proofs involving inats
Wed, 20 Feb 2008 18:28:16 +0100 huffman fix proofs involving ile_def
Thu, 17 Jan 2008 21:44:19 +0100 huffman rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
Wed, 16 Jan 2008 22:41:49 +0100 huffman change class axiom ax_flat to rule_format
Fri, 04 Jan 2008 23:24:32 +0100 huffman simplified some proofs
Tue, 23 Oct 2007 22:48:25 +0200 nipkow changed back from ~=0 to >0
Thu, 26 Apr 2007 14:24:08 +0200 wenzelm eliminated unnamed infixes, tuned syntax;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Fri, 02 Jun 2006 19:41:37 +0200 wenzelm tuned;
Wed, 03 May 2006 03:47:15 +0200 huffman update to reflect changes in inverts/injects lemmas
Thu, 13 Apr 2006 23:15:44 +0200 huffman add lemma less_UU_iff as default simp rule
Mon, 07 Nov 2005 19:03:02 +0100 wenzelm avoid 'as' as identifier;
Thu, 03 Nov 2005 00:43:50 +0100 huffman changed iterate to a continuous type
Tue, 06 Sep 2005 19:28:58 +0200 wenzelm converted to Isar theory format;
Thu, 07 Jul 2005 19:40:00 +0200 huffman fixes to work with UU_reorient_simproc
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 03 Jun 2005 23:37:21 +0200 huffman fixed some renamed theorems
Tue, 07 Sep 2004 16:02:42 +0200 oheimb integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Mon, 12 Apr 2004 12:18:48 +0200 oheimb added Streams.thy (with stream concatenation etc.)
Thu, 28 Aug 2003 01:56:40 +0200 skalberg Extended the notion of letter and digit, such that now one may use greek,
Sat, 03 Nov 2001 18:41:28 +0100 wenzelm GPLed;
Thu, 31 May 2001 16:52:47 +0200 oheimb added stream length, map, and filter
Wed, 28 Jun 2000 10:54:21 +0200 paulson tidying and unbatchifying
Tue, 04 Nov 1997 14:40:29 +0100 oheimb * removed "axioms" and "generated by" section
Fri, 31 Jan 1997 16:56:32 +0100 oheimb added Classlib.* and Witness.*,
less more (0) tip