| Tue, 05 Nov 2013 09:45:02 +0100 |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file | diff | annotate |
| Fri, 01 Nov 2013 18:51:14 +0100 |
more simplification rules on unary and binary minus
|
file | diff | annotate |
| Tue, 03 Sep 2013 00:51:08 +0200 |
proper imports;
|
file | diff | annotate |
| Tue, 27 Aug 2013 14:37:56 +0200 |
renamed typeclass dense_linorder to unbounded_dense_linorder
|
file | diff | annotate |
| Fri, 19 Oct 2012 15:12:52 +0200 |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file | diff | annotate |
| Fri, 12 Oct 2012 18:58:20 +0200 |
discontinued obsolete typedef (open) syntax;
|
file | diff | annotate |
| Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| Tue, 13 Mar 2012 16:56:56 +0100 |
prefer abs_def over def_raw;
|
file | diff | annotate |
| Wed, 30 Nov 2011 16:27:10 +0100 |
prefer typedef without extra definition and alternative name;
|
file | diff | annotate |
| Thu, 13 Jan 2011 23:50:16 +0100 |
eliminated global prems;
|
file | diff | annotate |
| Tue, 30 Nov 2010 17:19:11 +0100 |
adaptions to changes in Equiv_Relation.thy
|
file | diff | annotate |
| Fri, 01 Oct 2010 16:05:25 +0200 |
constant `contents` renamed to `the_elem`
|
file | diff | annotate |
| Mon, 12 Jul 2010 08:58:13 +0200 |
dropped superfluous [code del]s
|
file | diff | annotate |
| Tue, 08 Jun 2010 16:37:22 +0200 |
tuned quotes, antiquotations and whitespace
|
file | diff | annotate |
| Mon, 10 May 2010 11:47:56 -0700 |
add more credits to ex/Dedekind_Real.thy
|
file | diff | annotate |
| Mon, 10 May 2010 11:30:05 -0700 |
put construction of reals using Dedekind cuts in HOL/ex
|
file | diff | annotate |