| Mon, 27 Aug 2012 16:10:54 +0200 |
wenzelm |
clarified "isabelle logo";
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:47:16 +0200 |
wenzelm |
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
|
file |
diff |
annotate
|
| Fri, 17 Aug 2012 17:35:07 +0200 |
wenzelm |
some explanations on isabelle components;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 11:43:08 +0200 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2012 14:45:40 +0200 |
wenzelm |
discontinued obsolete "isabelle makeall";
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 23:43:05 +0200 |
wenzelm |
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2012 16:05:29 +0200 |
wenzelm |
"isabelle options" prints Isabelle system options;
|
file |
diff |
annotate
|
| Sun, 05 Aug 2012 20:11:32 +0200 |
wenzelm |
more on isabelle mkroot;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 12:37:31 +0200 |
wenzelm |
simplified custom document/build script, instead of old-style document/IsaMakefile;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 16:23:20 +0200 |
wenzelm |
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:18:15 +0200 |
wenzelm |
discontinued obsolete Isabelle/build script;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 20:12:47 +0200 |
wenzelm |
announce advanced support for Isabelle sessions and build management;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 13:11:58 +0200 |
wenzelm |
discontinued special treatment of Proof General;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 09:28:03 +0200 |
haftmann |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
file |
diff |
annotate
|
| Sun, 22 Jul 2012 10:00:51 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added MaSh to news
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 22:21:59 +0200 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
removed lie
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
doc updates
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:31:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:20:54 +0200 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
| Fri, 29 Jun 2012 15:45:50 +0200 |
wenzelm |
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 11:07:51 +0200 |
wenzelm |
updated "isar-ref" manual, reduced remaining material in "ref" manual.
|
file |
diff |
annotate
|
| Thu, 21 Jun 2012 13:51:44 +0200 |
bulwahn |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:07:23 +0200 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
| Tue, 29 May 2012 13:46:50 +0200 |
bulwahn |
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:01:17 +0200 |
wenzelm |
discontinued support for Poly/ML 5.2.1;
|
file |
diff |
annotate
|
| Wed, 23 May 2012 16:22:27 +0200 |
wenzelm |
discontinued obsolete method fastsimp / tactic fast_simp_tac;
|
file |
diff |
annotate
|
| Wed, 23 May 2012 12:02:27 +0200 |
wenzelm |
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 22:05:59 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Thu, 03 May 2012 22:07:29 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:43:57 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:31:15 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 20:15:31 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 17:23:41 +0200 |
huffman |
edit NEWS items for transfer/lifting
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 22:18:39 +1000 |
Gerwin Klein |
provide [[record_codegen]] option for skipping codegen setup for records
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 18:09:50 +0200 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 17:54:50 +0200 |
wenzelm |
updated system manual for release;
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 10:03:46 +0200 |
haftmann |
less confusion in NEWS
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:24:30 +0200 |
wenzelm |
mention tools and packages earlier;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:13:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:02:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 14:28:13 +0200 |
hoelzl |
sorted lemma list in NEWS
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 22:22:57 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:31:52 +0200 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 21:53:43 +0200 |
wenzelm |
typedef with implicit set definition is considered legacy;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 16:33:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
fixed typos
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:30:18 +0200 |
wenzelm |
USER_HOME settings variable points to cross-platform user home directory;
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 21:38:08 +0200 |
huffman |
update NEWS for transfer/quotient
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 13:54:29 +0200 |
huffman |
NEWS for transfer, lifting, and quotient
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 11:17:01 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 23:18:47 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 22:21:15 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 15:02:13 +0200 |
wenzelm |
more robust Sledgehammer in Prover IDE;
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:40:25 +0200 |
blanchet |
Sledgehammer NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 20:48:15 +0200 |
haftmann |
dropped errorneous NEWS entry
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 20:47:21 +0200 |
haftmann |
consolidated NEWS entries on fold
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 20:45:48 +0200 |
haftmann |
grouped fold-related NEWS entries together
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 20:40:52 +0200 |
haftmann |
grouped NEWS concerning relations together
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 20:38:15 +0200 |
haftmann |
merged rename traces
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 19:38:48 +0200 |
wenzelm |
repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 19:01:57 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 09:59:49 +0200 |
nipkow |
refined new tutorial announcement
|
file |
diff |
annotate
|
| Sun, 15 Apr 2012 14:50:09 +0200 |
wenzelm |
some coverage of bundled declarations;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2012 13:15:14 +0200 |
wenzelm |
some coverage of unnamed contexts, which can be nested within other targets;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 13:05:59 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 12:51:38 +0200 |
wenzelm |
revert changes of already published NEWS;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 12:46:45 +0200 |
wenzelm |
some updates for release;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 12:36:11 +0200 |
wenzelm |
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 13:30:27 +0200 |
Andreas Lochbihler |
Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 13:29:55 +0200 |
Andreas Lochbihler |
NEWS
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 09:17:01 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 11 Apr 2012 21:40:46 +0200 |
wenzelm |
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 11:42:15 +0200 |
wenzelm |
some coverage of HOL/TPTP;
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 19:23:51 +0200 |
haftmann |
abandoned almost redundant *_foldr lemmas
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 18:17:16 +0200 |
haftmann |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 14:08:24 +0200 |
bulwahn |
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 13:47:00 +0200 |
nipkow |
new tutorial
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 22:55:06 +0200 |
krauss |
less modest NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 22:41:56 +0200 |
krauss |
renamed import session back to Import, conforming to directory name; NEWS
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 11:16:35 +0200 |
huffman |
removed redundant nat-specific copies of theorems
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 09:04:29 +0200 |
haftmann |
power on predicate relations
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 17:40:44 +0200 |
bulwahn |
announcing NEWS (cf. 446cfc760ccf)
|
file |
diff |
annotate
|
| Wed, 28 Mar 2012 13:53:30 +0200 |
wenzelm |
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
|
file |
diff |
annotate
|
| Wed, 28 Mar 2012 08:25:51 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 20:19:23 +0200 |
huffman |
remove more redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:04:51 +0200 |
huffman |
generalized lemma zpower_zmod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:53:48 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:40:11 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:34:04 +0200 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:27:49 +0200 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| Wed, 28 Mar 2012 00:18:11 +0200 |
wenzelm |
updated to jedit-4.5.1;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sat, 24 Mar 2012 20:24:16 +0100 |
wenzelm |
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| 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
|