| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 13:34:24 +0200 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 13:21:23 +0200 |
wenzelm |
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 11:13:33 +0200 |
hoelzl |
clarified NEWS entry
|
file |
diff |
annotate
|
| Wed, 12 May 2010 11:08:15 +0200 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Wed, 12 May 2010 11:07:46 +0200 |
hoelzl |
added NEWS entry
|
file |
diff |
annotate
|
| Tue, 11 May 2010 12:05:19 -0700 |
huffman |
removed lemma real_sq_order; use power2_le_imp_le instead
|
file |
diff |
annotate
|
| Tue, 11 May 2010 11:58:34 -0700 |
huffman |
fix spelling of 'superseded'
|
file |
diff |
annotate
|
| Tue, 11 May 2010 11:57:14 -0700 |
huffman |
NEWS: removed theory PReal
|
file |
diff |
annotate
|
| Tue, 11 May 2010 11:40:39 -0700 |
huffman |
collected NEWS updates for HOLCF
|
file |
diff |
annotate
|
| Tue, 11 May 2010 08:36:02 +0200 |
haftmann |
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
|
file |
diff |
annotate
|
| Tue, 11 May 2010 08:29:42 +0200 |
haftmann |
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:59:19 +0200 |
haftmann |
dropped duplicate comp_arith
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:44:30 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:34 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:38:18 +0200 |
wenzelm |
old NEWS on global operations;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 20:00:26 +0200 |
wenzelm |
removed some Emacs junk;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 18:41:38 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:39 +0200 |
haftmann |
NEWS: code_reflect
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:47:53 +0200 |
wenzelm |
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:29:57 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:29:39 +0200 |
haftmann |
empty class specifcations observe default sort
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:21:55 +0200 |
wenzelm |
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 08:25:02 +0200 |
haftmann |
term_typ: print styled term
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 21:46:10 +0200 |
wenzelm |
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 10:42:41 +0200 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:45:08 +0200 |
wenzelm |
command 'example_proof' opens an empty proof body;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:15 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 22:48:07 +0200 |
wenzelm |
explicit 'schematic_theorem' etc. for schematic theorem statements;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 13:58:14 +0200 |
haftmann |
modernized abstract algebra theories
|
file |
diff |
annotate
|