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