| Thu, 11 Aug 2016 18:26:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 07:36:58 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 15:42:52 +0200 |
nipkow |
"split add" -> "split".
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 12:30:31 +0200 |
eberlm |
Tuned primes
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
|
| Sat, 06 Aug 2016 18:14:59 +0200 |
wenzelm |
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:30:53 +0200 |
wenzelm |
Sidekick parser for isabelle-ml and sml mode;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2016 21:25:16 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2016 11:45:09 +0200 |
wenzelm |
include 'begin' and 'end' structure in text folds;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 18:11:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:35:18 +0200 |
wenzelm |
support 'abbrevs' within theory header;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 08:22:59 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Sun, 24 Jul 2016 16:48:39 +0200 |
haftmann |
text antiquotation for locales (similar to classes)
|
file |
diff |
annotate
|
| Wed, 27 Jul 2016 10:44:22 +0200 |
Manuel Eberl |
NEWS: Primes
|
file |
diff |
annotate
|
| Thu, 21 Jul 2016 10:52:27 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 22:36:10 +0200 |
wenzelm |
provide Pure.simp/simp_all, which only know about meta-equality;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 16:02:00 +0200 |
wenzelm |
completion templates for commands involving "begin ... end" blocks;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 11:44:11 +0200 |
wenzelm |
moved method "use" to Pure;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 14:52:09 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 13:51:38 +0200 |
fleury |
adding mset_map to the simp rules
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 00:38:33 +0200 |
wenzelm |
information about proof outline with cases (sendback);
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 15:19:16 +0200 |
wenzelm |
semantic indentation for unstructured proof scripts;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 16:04:19 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 14:53:47 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 13:55:35 +0200 |
fleury |
sharing simp rules between ordered monoids and rings
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 11:51:05 +0200 |
wenzelm |
added action "isabelle.newline" (shortcut ENTER);
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 22:07:02 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 22:02:18 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 21:02:26 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Fri, 08 Jul 2016 23:43:11 +0200 |
haftmann |
avoid to hide equality behind (output) abbreviation
|
file |
diff |
annotate
|
| Fri, 08 Jul 2016 19:35:31 +0200 |
nipkow |
new style dummy_pats
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 17:34:39 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Wed, 06 Jul 2016 23:19:28 +0200 |
blanchet |
leverage new 'order' type class instantiation in multiset
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 13:05:04 +0200 |
fleury |
instantiate multiset with multiset ordering
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 20:51:04 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 20:48:55 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:49:25 +0200 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:20 +0200 |
haftmann |
combinator to build partial equivalence relations from a predicate and an equivalenc relation
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:20 +0200 |
haftmann |
basic facts about almost everywhere fix bijections
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:19 +0200 |
haftmann |
dedicated locale for total bijections
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 23:10:19 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 16:46:36 +0200 |
haftmann |
compiling implicit instances into companion objects for classes avoids ambiguities
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 12:37:43 +0200 |
fleury |
normalising multiset theorem names
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 16:39:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 20:48:41 +0200 |
haftmann |
explicit resolution of ambiguous dictionaries
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 13:57:59 +0200 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 23:13:04 +0200 |
wenzelm |
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 22:47:25 +0200 |
wenzelm |
added command 'unbundle';
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 12:45:34 +0200 |
wenzelm |
prefer hybrid 'bundle' command;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 17:14:13 +0200 |
wenzelm |
documentation;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 18:46:09 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 18:45:50 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 09:09:46 +0200 |
Andreas Lochbihler |
repair Unicode mess-up in c493859d4267
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 09:07:05 +0200 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for SPMF
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:45 +0200 |
haftmann |
conventional syntax for unit abstractions
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 16:04:26 +0200 |
wenzelm |
added action "isabelle.select-entity";
|
file |
diff |
annotate
|
| Sat, 04 Jun 2016 16:23:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 04 Jun 2016 16:10:44 +0200 |
wenzelm |
Integer.lcm normalizes the sign as in HOL/GCD.thy;
|
file |
diff |
annotate
|
| Fri, 03 Jun 2016 22:27:01 +0200 |
wenzelm |
support for .scala tools;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 21:24:51 +0200 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 19:54:26 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 19:23:18 +0200 |
wenzelm |
more adhoc overloading;
|
file |
diff |
annotate
|
| Tue, 31 May 2016 21:54:10 +0200 |
wenzelm |
ad-hoc overloading for standard operations on type Rat.rat;
|
file |
diff |
annotate
|
| Mon, 30 May 2016 20:58:54 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Sat, 28 May 2016 21:38:58 +0200 |
wenzelm |
clarified 'axiomatization';
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:18 +0200 |
haftmann |
explicit check that abstract constructors cannot be part of official interface
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:17 +0200 |
haftmann |
do not export abstract constructors in code_reflect
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:10:48 +0200 |
nipkow |
added subtheory of longest common prefix
|
file |
diff |
annotate
|
| Thu, 26 May 2016 16:57:14 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:31:04 +0200 |
haftmann |
examples and documentation for code generator time measurements
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
delegate inclusion of required dictionaries to user-space instead of half-working magic
|
file |
diff |
annotate
|
| Thu, 26 May 2016 09:05:00 +0200 |
nipkow |
added function "prefixes" and some lemmas
|
file |
diff |
annotate
|
| Wed, 25 May 2016 17:40:56 +0200 |
nipkow |
renamed suffix(eq)
|
file |
diff |
annotate
|
| Wed, 25 May 2016 12:24:00 +0200 |
eberlm |
NEWS: Permutations of a set and randomised folds
|
file |
diff |
annotate
|
| Tue, 24 May 2016 15:16:57 +0200 |
wenzelm |
cartouche abbreviations work both for " as well;
|
file |
diff |
annotate
|
| Tue, 24 May 2016 11:39:26 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 22:43:22 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Mon, 23 May 2016 22:43:11 +0200 |
nipkow |
renamed prefix* in Library/Sublist
|
file |
diff |
annotate
|
| Mon, 23 May 2016 18:04:45 +0200 |
blanchet |
generate Vampire 4.0 compatible output
|
file |
diff |
annotate
|
| Mon, 23 May 2016 15:30:13 +0200 |
wenzelm |
removed odd cases rule (see also 8cb42cd97579);
|
file |
diff |
annotate
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
file |
diff |
annotate
|
| Tue, 10 May 2016 14:04:44 +0100 |
paulson |
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 11:34:26 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:39:17 +0200 |
wenzelm |
'obtain' supports structured statements (similar to 'define');
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 19:41:39 +0200 |
wenzelm |
old 'def' is legacy;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 21:31:14 +0200 |
wenzelm |
added Isar command 'define';
|
file |
diff |
annotate
|
| Wed, 20 Apr 2016 11:44:25 +0200 |
wenzelm |
reactivated other_id reports (see also db929027e701, 8eda56033203);
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 12:06:34 +0200 |
wenzelm |
more IDE support for Isabelle/Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 15 Apr 2016 16:50:23 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 23:31:10 +0200 |
wenzelm |
highlighting of entity def/ref positions wrt. cursor;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:55:00 +0200 |
hoelzl |
change is incompatible
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:48:11 +0200 |
hoelzl |
Probability: move emeasure and nn_integral from ereal to ennreal
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 18:49:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 21:42:42 +0200 |
wenzelm |
removed old proof method "default";
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 19:30:15 +0200 |
wenzelm |
support ROOT0.ML as well -- independently of ROOT.ML;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:26:22 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 11:57:21 +0200 |
wenzelm |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 19:41:58 +0200 |
wenzelm |
clarified bootstrap environment;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:13:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:07:08 +0200 |
wenzelm |
option ML_system_unsafe;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 09:45:04 +0200 |
blanchet |
added reference from NEWS to docs
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 23:56:52 +0200 |
wenzelm |
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 21:34:51 +0200 |
wenzelm |
documentation;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
document addition of 'corec'
|
file |
diff |
annotate
|
| Sat, 19 Mar 2016 16:53:09 +0100 |
haftmann |
unified CHAR with CHR syntax
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 20:35:01 +0100 |
wenzelm |
recovered from Unicode accident in 7248d106c607;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 20:29:50 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 16:56:44 +0100 |
wenzelm |
@{make_string} is available during Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 08:01:49 +0100 |
Andreas Lochbihler |
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:19:08 +0100 |
wenzelm |
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:04:38 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:22:12 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|