| Wed, 03 Mar 2010 07:36:31 -0800 |
huffman |
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:20:03 -0800 |
huffman |
variable name changed
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 04:31:50 -0800 |
huffman |
re-enable bisim code, now in domain_theorems.ML
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 00:34:26 -0800 |
huffman |
domain package no longer generates copy functions; all proofs use take functions instead
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 16:15:03 -0800 |
huffman |
reorganizing domain package code (in progress)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:20:07 -0800 |
huffman |
change domain package's treatment of variable names in theorems to be like datatype package
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 13:29:59 -0800 |
huffman |
get rid of warnings about duplicate simp rules in all HOLCF theories
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 10:00:22 -0800 |
huffman |
remove $ from all HOLCF files
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 09:08:58 -0800 |
huffman |
fix warnings about duplicate simp rules
|
file |
diff |
annotate
|
| 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
|