| Mon, 11 Oct 2010 21:35:31 -0700 |
huffman |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file |
diff |
annotate
|
| Sat, 09 Oct 2010 07:24:49 -0700 |
huffman |
move all bifinite class instances to Bifinite.thy
|
file |
diff |
annotate
|
| Fri, 08 Oct 2010 07:39:50 -0700 |
huffman |
rename class 'sfp' to 'bifinite'
|
file |
diff |
annotate
|
| Thu, 07 Oct 2010 13:54:43 -0700 |
huffman |
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
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 23:34:23 -0700 |
huffman |
completely remove constants cpair, cfst, csnd
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 22:55:26 -0700 |
huffman |
define csplit using fst, snd
|
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
|
| Mon, 02 Nov 2009 17:19:49 -0800 |
huffman |
add (LAM (x, y). t) syntax and lemma csplit_Pair
|
file |
diff |
annotate
|
| Mon, 11 May 2009 12:26:33 -0700 |
huffman |
move bifinite instance for product type from Cprod.thy to Bifinite.thy
|
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
|
| Thu, 15 Jan 2009 08:11:50 -0800 |
huffman |
add strictness and compactness lemmas to Product_Cpo.thy
|
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: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
|
| Sat, 02 Feb 2008 03:28:36 +0100 |
huffman |
instance "*" :: (sq_ord, sq_ord) sq_ord
|
file |
diff |
annotate
|
| Fri, 01 Feb 2008 02:38:41 +0100 |
huffman |
add lemmas prod_lessI and Pair_less_iff [simp]
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:48:14 +0100 |
huffman |
add lemma cpo_lubI
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 21:23:14 +0100 |
huffman |
instances for class discrete_cpo
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 01:31:19 +0100 |
huffman |
new lemma is_lub_Pair; cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 17 Jan 2008 00:51:20 +0100 |
huffman |
change class axiom chfin to rule_format
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 02:18:01 +0100 |
huffman |
declare cpair_strict [simp]
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 21:16:06 +0100 |
huffman |
add bifinite instances
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:45:10 +0100 |
huffman |
cleaned up instance proofs
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 20:35:52 +0100 |
huffman |
new-style instantiation proof for unit :: po
|
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 20:04:40 +0100 |
huffman |
simplified chfin instance proof
|
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
|
| Thu, 03 Jan 2008 22:10:52 +0100 |
huffman |
instance unit :: finite_po
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 18:29:03 +0100 |
huffman |
update instance proofs for sq_ord, po; new instance proofs for dcpo
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 00:53:30 +0100 |
huffman |
add constant unit_when
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:11:39 +0100 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 01:02:29 +0100 |
huffman |
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 01:43:37 +0200 |
huffman |
added compactness lemmas; cleaned up
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 23:27:14 +0200 |
huffman |
added xsymbols syntax for pairs; cleaned up
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 05:30:02 +0200 |
huffman |
new syntax translations for continuous lambda abstraction
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 18:22:03 +0200 |
huffman |
add theorem cpair_defined_iff
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:37:42 +0200 |
huffman |
add lemma eq_cprod
|
file |
diff |
annotate
|
| Thu, 23 Jun 2005 22:07:30 +0200 |
huffman |
add csplit3, ssplit3, fup3 as simp rules
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 00:07:46 +0200 |
huffman |
added theorem less_cprod
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:26:32 +0200 |
huffman |
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
|
file |
diff |
annotate
|
| Fri, 27 May 2005 00:16:18 +0200 |
huffman |
use thelub_const lemma
|
file |
diff |
annotate
|
| Thu, 26 May 2005 02:23:27 +0200 |
huffman |
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
|
file |
diff |
annotate
|
| Wed, 25 May 2005 09:44:34 +0200 |
wenzelm |
removed LICENCE note -- everything is subject to Isabelle licence as
|
file |
diff |
annotate
|
| Tue, 24 May 2005 05:32:19 +0200 |
huffman |
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
|
file |
diff |
annotate
|
| Thu, 19 May 2005 02:33:40 +0200 |
huffman |
pcpo instance for type unit
|
file |
diff |
annotate
|
| Mon, 14 Mar 2005 20:30:43 +0100 |
huffman |
fixed syntax for Let <x,y> = a in e
|
file |
diff |
annotate
|
| Thu, 10 Mar 2005 20:22:45 +0100 |
huffman |
fixed filename in header
|
file |
diff |
annotate
|
| Tue, 08 Mar 2005 00:32:10 +0100 |
huffman |
reordered and arranged for document generation, cleaned up some proofs
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
file |
diff |
annotate
|