| Fri, 26 Nov 2010 15:24:11 -0800 |
huffman |
remove map function names from domain package theory data
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 08:47:58 -0800 |
huffman |
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 11:50:05 -0800 |
huffman |
rename 'repdef' to 'domaindef'
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:30:17 -0800 |
huffman |
merge Representable.thy into Domain.thy
|
file |
diff |
annotate
|
| Wed, 10 Nov 2010 18:15:21 -0800 |
huffman |
move stuff from Domain.thy to Domain_Aux.thy
|
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
|
| Tue, 19 Oct 2010 15:01:51 -0700 |
huffman |
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 14:28:14 -0700 |
huffman |
simplify some proofs; remove some unused lists of lemmas
|
file |
diff |
annotate
|
| Sat, 16 Oct 2010 16:22:42 -0700 |
huffman |
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:21:05 -0700 |
huffman |
add rule deflation_ID to proof script for take + constructor rules
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:33:05 -0800 |
huffman |
move lemmas from Domain.thy to Domain_Aux.thy
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 14:50:37 -0800 |
huffman |
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 20:19:04 -0800 |
huffman |
remove dependency on domain_syntax.ML
|
file |
diff |
annotate
|