| Thu, 22 Mar 2012 18:37:20 +0100 |
haftmann |
more instructive NEWS
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 16:07:03 +0100 |
wenzelm |
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 11:57:03 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 08:00:18 +0100 |
haftmann |
generalized INF_INT_eq, SUP_UN_eq
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 09:51:18 +0100 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:21:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 16:32:34 +0000 |
paulson |
ZF news
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 14:42:11 +0100 |
wenzelm |
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 23:06:22 +0100 |
wenzelm |
Isabelle/jEdit supports user-defined Isar commands within the running session;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:48:19 +0100 |
wenzelm |
added ML antiquotation @{keyword};
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 11:45:16 +0100 |
wenzelm |
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:22:18 +0100 |
wenzelm |
improved attribute "abs_def" to handle object-equality as well;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:34:45 +0100 |
noschinl |
NEWS
|
file |
diff |
annotate
|
| Wed, 07 Mar 2012 21:38:29 +0100 |
haftmann |
less rigorous but more realistic migration recommendation; note on code generation of sets
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 15:54:51 +0100 |
blanchet |
spelling
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 18:08:27 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sat, 18 Feb 2012 23:05:31 +0100 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 21:08:27 +0100 |
wenzelm |
discontinued obsolete "prems" fact;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 19:31:27 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 16:59:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 07:11:04 +0100 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
docs and news
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:28 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 11:15:36 +0100 |
bulwahn |
refreshing NEWS
|
file |
diff |
annotate
|
| Mon, 16 Jan 2012 21:50:15 +0100 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 10:48:39 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 09 Jan 2012 14:47:18 +0100 |
wenzelm |
misc tuning and reformatting;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 21:48:45 +0100 |
haftmann |
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:53:52 +0100 |
haftmann |
more explicit NEWS
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 18:18:39 +0100 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 12:55:37 +0100 |
huffman |
fix typos
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 12:52:23 +0100 |
huffman |
remove some duplicate lemmas
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:15:26 +0100 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
NEWS: unavoidable fact renames
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:59 +0100 |
haftmann |
NEWS: `set` is now a proper type constructor
|
file |
diff |
annotate
|
| Fri, 23 Dec 2011 15:55:23 +0100 |
huffman |
remove redundant lemma word_sub_def
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 09:39:14 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 17:49:42 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 22:00:42 +0100 |
huffman |
prove class instances without extra lemmas
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 14:52:51 +0100 |
huffman |
remove redundant lemma word_diff_minus
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:03 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 13:10:19 +0100 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:14 +0100 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:13 +0100 |
blanchet |
renamed "slicing" to "slice"
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 12:25:27 +0100 |
wenzelm |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Mon, 21 Nov 2011 23:29:53 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:44:41 +0100 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:23:16 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 15:07:46 +0100 |
huffman |
HOL-Word: removed more duplicate theorems
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 14:52:05 +0100 |
huffman |
HOL-Word: removed many duplicate theorems (see NEWS)
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 10:34:08 +0100 |
blanchet |
document "lam_trans" option
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 17:57:42 +0100 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 22:22:01 +0100 |
blanchet |
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 14:23:50 +0100 |
wenzelm |
clarified attribute "mono_set": pure declaration, proper export in ML;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 14:14:20 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:16 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 22:54:26 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 15:42:43 +0200 |
wenzelm |
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:21 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 14:22:14 +0200 |
noschinl |
(old) NEWS
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 18:55:29 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 11:45:33 +0200 |
wenzelm |
discontinued obsolete 'types' command;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 16:21:07 +0200 |
wenzelm |
discontinued obsolete alias structure ProofContext;
|
file |
diff |
annotate
|
| Sun, 09 Oct 2011 11:13:53 +0200 |
huffman |
Int.thy: discontinued some legacy theorems
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 21:13:26 +0200 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 21:09:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 20:53:53 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 12:55:19 -0700 |
huffman |
discontinued HOLCF legacy theorem names
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 10:02:16 -0400 |
hoelzl |
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 00:12:36 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 22:11:22 +0200 |
haftmann |
official status for UN_singleton
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 15:57:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 15:39:55 +0200 |
wenzelm |
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 14:48:25 +0200 |
wenzelm |
some tuning and re-ordering for release;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 14:34:24 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 17:06:00 +0200 |
noschinl |
NEWS on Complete_Lattices, Lattices
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:56:38 +0200 |
bulwahn |
correcting NEWS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 13:19:10 -0700 |
huffman |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:54:20 -0700 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:28:45 -0700 |
huffman |
fix typos
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:37:49 -0700 |
huffman |
NEWS for euclidean_space class
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:57:33 -0400 |
hoelzl |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 13:35:35 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:27:36 +0200 |
bulwahn |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:45:53 +0200 |
bulwahn |
tuned some symbol that probably went there by some strange encoding issue
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:05:32 +0200 |
blanchet |
added my contributions to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:07:23 +0200 |
nipkow |
NEWS fastsimp -> fastforce
|
file |
diff |
annotate
|
| Sun, 11 Sep 2011 13:49:42 -0700 |
huffman |
NEWS for Library/Product_Lattice.thy
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 19:24:28 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:45:39 -0700 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 00:23:23 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:10:47 +0200 |
wenzelm |
NEWS on IsabelleText font;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 20:49:45 +0200 |
wenzelm |
some updates for release;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 20:29:54 +0200 |
wenzelm |
some tuning for release;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 11:26:27 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 21:56:11 +0200 |
wenzelm |
some Isabelle/jEdit NEWS;
|
file |
diff |
annotate
|