| Mon, 09 Mar 2015 16:42:18 +0000 |
paulson |
Removed the infix operator "choose" to allow HOLCF to build
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:16:01 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Sun, 11 Mar 2012 13:54:08 +0100 |
wenzelm |
eliminated old-fashioned 'constrains' element;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 17:47:11 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 17:19:50 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Tue, 04 Jan 2011 15:32:56 -0800 |
huffman |
change some lemma names containing 'UU' to 'bottom'
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 18:24:04 -0800 |
huffman |
rename function ideal_completion.basis_fun to ideal_completion.extension
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 08:43:39 -0800 |
huffman |
declare more simp rules, rewrite proofs in Isar-style
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:11:20 -0800 |
huffman |
types -> type_synonym
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 05:15:31 -0800 |
huffman |
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 19:15:06 -0800 |
huffman |
add notsqsubseteq syntax
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:29:39 -0800 |
huffman |
reformulate lemma preorder.ex_ideal, and use it for typedefs
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 16:08:10 -0800 |
huffman |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file |
diff |
annotate
| base
|