| Fri, 26 Nov 2010 14:10:34 -0800 |
huffman |
declare more simp rules for powerdomains
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 13:37:17 -0800 |
huffman |
add bind_bind rules for powerdomains
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 12:08:28 -0800 |
huffman |
add lemmas about powerdomains
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 11:57:10 -0800 |
huffman |
declare {upper,lower,convex}_pd_induct as default induction rules
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 11:42:35 -0800 |
huffman |
rename class 'bifinite' to 'domain'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 08:18:32 -0800 |
huffman |
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 16:37:13 -0800 |
huffman |
add 'predomain' class: unpointed version of bifinite
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 06:58:09 -0800 |
huffman |
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 15:15:28 -0700 |
huffman |
(infixl "<<" 55) -> (infix "<<" 50)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 17:15:28 -0700 |
huffman |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
file |
diff |
annotate
|
| 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
|
| Mon, 11 Oct 2010 08:32:09 -0700 |
huffman |
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
|
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:33:06 -0700 |
huffman |
add lemma typedef_ideal_completion
|
file |
diff |
annotate
|