| 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
|
| Wed, 02 Jan 2008 18:54:21 +0100 |
huffman |
remove not_up_less_UU [simp]
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 02:11:27 +0100 |
huffman |
use minimal imports
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 00:55:24 +0100 |
huffman |
add xsymbol syntax for u type constructor
|
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
|
| Wed, 12 Oct 2005 03:01:09 +0200 |
huffman |
added compactness theorems
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 19:06:05 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:48 +0200 |
wenzelm |
fixed var index in tactic;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:41:19 +0200 |
huffman |
define 'a u with datatype package;
|
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 23:43:19 +0200 |
huffman |
make up_eq and up_less into simp rules
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 01:40:39 +0200 |
huffman |
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:34:49 +0200 |
huffman |
changed to use new contlubI, etc.
|
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
|
| Thu, 10 Mar 2005 20:19:55 +0100 |
huffman |
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
|
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
|