src/HOLCF/FOCUS/Stream_adm.thy
Sun, 10 May 2009 14:21:41 +0200 nipkow fixed HOLCF proofs
Tue, 01 Jul 2008 02:19:53 +0200 huffman replace lub (range Y) with (LUB i. Y i)
Tue, 10 Jun 2008 14:32:58 +0200 haftmann slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
Wed, 07 May 2008 10:59:53 +0200 berghofe Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma
Thu, 27 Mar 2008 19:22:24 +0100 wenzelm avoid amiguity of Continuity.chain vs. Porder.chain;
Wed, 20 Feb 2008 18:28:16 +0100 huffman fix proofs involving ile_def
Tue, 31 Jul 2007 23:23:34 +0200 wenzelm proper path specifications;
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;
Thu, 01 Jun 2006 23:53:29 +0200 huffman removed legacy ML scripts
Thu, 03 Nov 2005 00:43:50 +0100 huffman changed iterate to a continuous type
Tue, 06 Sep 2005 21:51:17 +0200 wenzelm converted to Isar theory format;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 03 Oct 2001 20:54:16 +0200 wenzelm tuned parentheses in relational expressions;
Thu, 31 May 2001 20:52:51 +0200 wenzelm tuned
Thu, 31 May 2001 16:53:00 +0200 oheimb added FOCUS including the One-Element Buffer by Manfred Broy
less more (0) tip