| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 12:04:18 +0200 |
nipkow |
renamed expand_*_eq in HOLCF as well
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 12:52:51 -0700 |
huffman |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 22:00:34 -0800 |
huffman |
declare case_names for various induction rules
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 23:59:54 +0100 |
wenzelm |
proper (type_)notation;
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 21:44:37 -0800 |
huffman |
add map_ID lemmas
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 15:51:32 -0800 |
huffman |
add map_map lemmas
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:47:00 -0800 |
huffman |
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
|
file |
diff |
annotate
|
| Fri, 08 May 2009 16:19:51 -0700 |
huffman |
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 17:11:29 -0800 |
huffman |
change to simpler, more extensible continuity simproc
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 02:50:29 +0200 |
huffman |
remove unused lemma is_lub_Iup'
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 02:19:53 +0200 |
huffman |
replace lub (range Y) with (LUB i. Y i)
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 23:01:09 +0200 |
huffman |
simplify profinite class axioms
|
file |
diff |
annotate
|
| Mon, 19 May 2008 23:49:20 +0200 |
huffman |
use new class package for classes profinite, bifinite; remove approx class
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:38:17 +0100 |
huffman |
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
|
file |
diff |
annotate
|
| Thu, 07 Feb 2008 03:30:32 +0100 |
huffman |
fix broken syntax translations
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:48:14 +0100 |
huffman |
add lemma cpo_lubI
|
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
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 21:42:58 +0100 |
huffman |
added bifinite class instance
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:28:59 +0100 |
huffman |
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 03:58:30 +0100 |
huffman |
compact_chfin is now declared simp
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 05:15:43 +0100 |
huffman |
new compactness lemmas
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 00:01:02 +0100 |
huffman |
new instance proofs for classes finite_po, chfin, flat
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 20:23:49 +0100 |
huffman |
add dcpo instance proof
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 19:51:29 +0100 |
huffman |
declare upE as cases rule; add new rule up_induct
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 19:41:12 +0100 |
huffman |
update sq_ord/po instance proofs
|
file |
diff |
annotate
|