| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 17:51:34 +0100 |
blanchet |
more multiset theorems
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:59:28 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 15:57:51 +0100 |
wenzelm |
admit dummy patterns in instantiations;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 23:16:40 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 17:23:22 +0000 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 13:51:33 +0100 |
noschinl |
added proof method rewrite
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 23:04:40 +0100 |
blanchet |
documented renamed theories
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 21:30:42 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 20:33:33 +0100 |
wenzelm |
support structural composition (THEN_ALL_NEW) for proof methods;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 16:42:18 +0000 |
paulson |
Removed the infix operator "choose" to allow HOLCF to build
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 22:38:11 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:13 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:04 +0100 |
nipkow |
Removed the obsolete functions "natfloor" and "natceiling"
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2015 08:50:00 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Fri, 27 Feb 2015 15:41:28 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:50:30 +0100 |
wenzelm |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:48 +0100 |
haftmann |
eliminated fact duplicates
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:15 +0100 |
haftmann |
dropped redundancy
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:53:56 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 13:01:12 +0100 |
haftmann |
dropped obsolete external entrance point
|
file |
diff |
annotate
|
| Mon, 26 Jan 2015 14:34:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 25 Jan 2015 22:11:06 +0100 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 20:01:48 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Tue, 06 Jan 2015 22:48:34 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 11:12:15 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 11:08:47 +0100 |
boehmes |
updated NEWS
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 11:50:34 +0100 |
wenzelm |
added system property isabelle.laf, notably for initial system dialog;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 10:38:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 20:40:37 +0100 |
wenzelm |
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 16:44:24 +0100 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
| Fri, 12 Dec 2014 14:31:57 +0100 |
wenzelm |
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 12:30:47 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 16:55:43 +0100 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:44 +0100 |
immler |
NEWS
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 16:47:45 +0100 |
wenzelm |
added update_header tool;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2014 13:52:54 +0100 |
wenzelm |
'notepad' requires proper nesting of begin/end;
|
file |
diff |
annotate
|
| Sun, 26 Oct 2014 15:57:10 +0100 |
wenzelm |
clarified default;
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:49 +0200 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:55:45 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:35:45 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 16:52:36 +0200 |
wenzelm |
official support for "tt" style variants, avoid fragile \verb in LaTeX;
|
file |
diff |
annotate
|
| Sun, 19 Oct 2014 12:47:34 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 18 Oct 2014 22:49:59 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 17:05:34 +0200 |
haftmann |
generalized and consolidated some theorems concerning divisibility
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 11:09:17 +0200 |
wenzelm |
simplified "sos" method;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 09:09:12 +0200 |
Andreas Lochbihler |
move Code_Test to HOL/Library;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 14:53:51 +0200 |
wenzelm |
added update_cartouches tool;
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:55:49 +0200 |
wenzelm |
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 16:54:35 +0200 |
wenzelm |
completion for bibtex entries;
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 22:22:40 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 04 Oct 2014 22:15:31 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sat, 04 Oct 2014 22:15:22 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 03 Oct 2014 14:46:26 +0200 |
wenzelm |
SideKick parser for bibtex entries;
|
file |
diff |
annotate
|
| Fri, 03 Oct 2014 11:03:37 +0200 |
wenzelm |
context menu for bibtex entries;
|
file |
diff |
annotate
|
| Thu, 02 Oct 2014 11:33:06 +0200 |
haftmann |
moved lemmas out of Int.thy which have nothing to do with int
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 21:28:57 +0200 |
wenzelm |
discontinued old "xnum" token category;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 15:07:43 +0200 |
haftmann |
product over monoids for lists
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 07:38:15 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 17:50:54 +0200 |
nipkow |
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 17:51:32 +0200 |
haftmann |
restrictive options for class dependencies
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Sun, 31 Aug 2014 09:10:41 +0200 |
haftmann |
restored generic value slot, retaining default behaviour and separate approximate command
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 07:34:23 +0200 |
blanchet |
tuned terminology
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 07:30:16 +0200 |
blanchet |
moved new para to right section of NEWS
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
minor NEWS fix
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 13:05:59 +0200 |
blanchet |
removed not so interesting 'set_empty'
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 18:21:29 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 17:00:44 +0200 |
wenzelm |
added PARALLEL_ALLGOALS convenience;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:34:27 +0200 |
blanchet |
documented slight incompatibility in NEWS
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 12:10:36 +0200 |
wenzelm |
updated documentation concerning 'named_theorems';
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 14:34:43 +0200 |
wenzelm |
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
|
file |
diff |
annotate
|
| Fri, 08 Aug 2014 11:43:08 +0200 |
wenzelm |
improved monitor panel;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 17:55:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 31 Jul 2014 21:29:31 +0200 |
wenzelm |
completion popup supports both ENTER and TAB (default);
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 16:44:54 +0200 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| Tue, 29 Jul 2014 17:13:25 +0200 |
hoelzl |
better ordering of positive_integral renaming to nn_integral in NEWS
|
file |
diff |
annotate
|
| Mon, 28 Jul 2014 11:03:28 +0200 |
wenzelm |
some actual workaround to remove document nodes;
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Sun, 27 Jul 2014 15:44:08 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Sun, 27 Jul 2014 15:25:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 16:21:50 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 10:22:34 +0200 |
wenzelm |
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 16:04:45 +0200 |
wenzelm |
clarified "simp_trace_new" and corresponding isar-ref section;
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
tuned terminology
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 12:04:25 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:06:14 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 16:50:57 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 14:52:05 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 11:39:34 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 17:34:45 +0200 |
wenzelm |
tuned grammar and spelling (cf. 0cf15843b82f);
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 17:16:11 +0200 |
immler |
overdue NEWS concerning c4daa97ac57a
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:08:31 +0100 |
paulson |
for new release
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 14:52:08 +0200 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 10:53:37 +0200 |
wenzelm |
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 09:43:44 +0200 |
wenzelm |
"isabelle tty" is superseded by "isabelle console";
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
killed Python version of MaSh, now that the SML version works adequately
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 22:13:23 +0200 |
haftmann |
tracing facilities for the code generator preprocessor
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 15:50:48 +0200 |
wenzelm |
updated NEWS -- removed material that is already in the manual;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 15:30:57 +0200 |
wenzelm |
removed obsolete "isabelle unsymbolize";
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 13:23:09 +0200 |
blanchet |
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
|
file |
diff |
annotate
|
| Fri, 13 Jun 2014 14:49:59 +0100 |
paulson |
NEWS
|
file |
diff |
annotate
|
| Fri, 13 Jun 2014 14:08:20 +0200 |
hoelzl |
properties of normal distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
| Fri, 13 Jun 2014 07:05:01 +0200 |
nipkow |
announce Tree
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:50:49 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
updated NEWS slightly
|
file |
diff |
annotate
|
| Thu, 29 May 2014 16:13:47 +0200 |
nipkow |
removed Kleene_Algebra because of superior AFP entry; authors agreed
|
file |
diff |
annotate
|
| Tue, 27 May 2014 17:32:42 +0200 |
blanchet |
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Mon, 26 May 2014 14:15:48 +0200 |
blanchet |
renamed 'MaSh' option
|
file |
diff |
annotate
|
| Sat, 24 May 2014 20:24:43 +0200 |
wenzelm |
support for regular Windows TeX installation;
|
file |
diff |
annotate
|
| Tue, 20 May 2014 22:28:44 +0200 |
blanchet |
added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
|
file |
diff |
annotate
|
| Tue, 20 May 2014 22:28:08 +0200 |
blanchet |
added Isabelle system option 'mash'
|
file |
diff |
annotate
|
| Tue, 20 May 2014 16:46:42 +0200 |
blanchet |
news
|
file |
diff |
annotate
|
| Mon, 19 May 2014 14:26:58 +0200 |
hoelzl |
renamed positive_integral to nn_integral
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|
| Thu, 15 May 2014 18:18:50 +0200 |
haftmann |
type
|
file |
diff |
annotate
|
| Tue, 13 May 2014 09:21:22 +0200 |
traytel |
bnf_decl -> bnf_axiomatization
|
file |
diff |
annotate
|
| Mon, 12 May 2014 12:38:17 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:37 +0200 |
haftmann |
hardcoded nbe and sml into value command
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:36 +0200 |
haftmann |
prefer separate command for approximation
|
file |
diff |
annotate
|
| Wed, 07 May 2014 14:54:06 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
file |
diff |
annotate
|
| Tue, 06 May 2014 16:57:17 +0200 |
wenzelm |
renamed "Find" to "Query", with more general operations;
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:57:45 +0200 |
blanchet |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:53:58 +0200 |
blanchet |
added 'satx' proof method to Try0
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Sun, 04 May 2014 16:17:53 +0200 |
boehmes |
removed obsolete internal SAT solvers
|
file |
diff |
annotate
|
| Sat, 03 May 2014 22:47:43 +0200 |
wenzelm |
support for path completion based on file-system content;
|
file |
diff |
annotate
|
| Fri, 02 May 2014 23:31:25 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 02 May 2014 23:30:47 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 02 May 2014 21:18:50 +0200 |
haftmann |
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:32 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 15:42:19 +0200 |
wenzelm |
require explicit 'document_files';
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 22:57:51 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 22:51:21 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 21:37:09 +1000 |
kleing |
retired wwwfind
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 17:23:05 +0200 |
wenzelm |
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 22:41:10 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 19:11:34 +0200 |
wenzelm |
clarified abbreviations for cartouche delimiters, to work in any context;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 00:07:07 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 21:58:58 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 11:52:28 +0200 |
wenzelm |
explicit 'document_files' in session ROOT specifications;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 10:30:32 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 17:54:09 +0200 |
wenzelm |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 16:37:57 +0200 |
wenzelm |
refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:59:41 +0200 |
wenzelm |
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 22:51:22 +0200 |
wenzelm |
support for jEdit Navigator plugin;
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 12:07:48 +0200 |
wenzelm |
added ML antiquotation @{print};
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 17:56:08 +0200 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:01 +0200 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 21:13:51 +0200 |
wenzelm |
cumulative NEWS;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 08:59:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:54:38 +0100 |
wenzelm |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 14:52:35 +0100 |
wenzelm |
some SML examples;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 12:00:17 +0100 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 08:37:43 +0100 |
haftmann |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 22:00:13 +0100 |
wenzelm |
more static checking of proof methods;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 15:35:07 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 22:11:46 +0100 |
haftmann |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 17:32:11 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 11:34:05 +0100 |
wenzelm |
added ML antiquotation @{path};
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 01:28:13 +0100 |
blanchet |
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 08:56:08 +0100 |
haftmann |
dropped redundant theorems
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 22:57:50 +0100 |
wenzelm |
tuned signature -- clarified module name;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 22:44:55 +0100 |
wenzelm |
added ML antiquotation @{here};
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 21:58:48 +0100 |
wenzelm |
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 22:15:01 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 21:33:15 +0100 |
wenzelm |
some NEWS;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:29:18 +0100 |
blanchet |
renamed 'prod_rel' to 'rel_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:25:21 +0100 |
blanchet |
renamed 'sum_rel' to 'rel_sum'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:14:09 +0100 |
blanchet |
renamed 'filter_rel' to 'rel_filter'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:10:56 +0100 |
blanchet |
renamed 'vset_rel' to 'rel_vset'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:15 +0100 |
blanchet |
fixed NEWS
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:50 +0100 |
blanchet |
renamed 'cset_rel' to 'rel_cset'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:49 +0100 |
blanchet |
renamed 'fset_rel' to 'rel_fset'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:15 +0100 |
blanchet |
renamed 'map_sum' to 'sum_map'
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 14:22:35 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 17:08:39 +0100 |
haftmann |
more precise imports;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 13:18:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:44:57 +0100 |
haftmann |
NEWS and documentation, including correction of long-overseen "*"
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
dropped long-unused option
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 16:16:21 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 17:00:45 +0100 |
wenzelm |
improved completion based on context information;
|
file |
diff |
annotate
|