| Tue, 05 Jun 2018 18:08:13 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 21:57:43 +0200 |
wenzelm |
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 21:45:54 +0200 |
wenzelm |
tuned (see also 1fa1023b13b9);
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:16:01 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
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
|
| Fri, 24 Dec 2010 14:26:10 -0800 |
huffman |
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
|
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
|
| Wed, 15 Dec 2010 19:15:06 -0800 |
huffman |
add notsqsubseteq syntax
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 12:53:06 -0800 |
huffman |
simplify ideal completion proofs
|
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
|