| Sun, 02 Feb 2014 19:15:25 +0000 |
paulson |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 22:06:07 +0100 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:07:23 +0100 |
blanchet |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 21:32:41 +0100 |
blanchet |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
file |
diff |
annotate
|
| Thu, 28 Nov 2013 13:58:11 +0100 |
blanchet |
cleaned up indirect dependency
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:06:27 +0200 |
hoelzl |
renamed inner_dense_linorder to dense_linorder
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
lifting for primitive definitions;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 10:16:15 +0100 |
nipkow |
more lemmas about intervals
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
split dense into inner_dense_order and no_top/no_bot
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 10:52:47 +0100 |
Andreas Lochbihler |
added lemma
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:27 +0100 |
hoelzl |
introduce order topology
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 14:28:57 +0100 |
hoelzl |
add Int_atMost
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:25:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 15:15:00 +0200 |
huffman |
modernized obsolete old-style theory name with proper new-style underscore
|
file |
diff |
annotate
| base
|