| Mon, 15 May 2017 17:05:52 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 05 May 2017 11:16:13 +0200 |
Manuel Eberl |
NEWS: totient 1 = 1 now
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 15:56:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 11:23:07 +0200 |
wenzelm |
clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:10:23 +0200 |
wenzelm |
tuned documentation;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 15:59:51 +0200 |
wenzelm |
clarified tool name -- more official status;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:36:20 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 18:57:30 +0200 |
wenzelm |
afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 16:21:28 +0200 |
blanchet |
removed Old_SMT legacy module
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 16:24:59 +0200 |
wenzelm |
optionally explore all sessions -- potentially slow, e.g. for AFP;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 16:22:20 +0200 |
wenzelm |
proper sections;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 14:51:46 +0200 |
wenzelm |
some documentation;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 09:27:43 +0200 |
haftmann |
more fundamental euler's totient function on nat rather than int;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 21:06:19 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 20:17:00 +0200 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 09:01:19 +0200 |
eberlm |
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
|
file |
diff |
annotate
|
| Sun, 19 Mar 2017 20:28:21 +0100 |
wenzelm |
updated to jedit-5.4.0;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 13:47:35 +0100 |
haftmann |
restored surj as output abbreviation, amending 6af79184bef3
|
file |
diff |
annotate
|
| Thu, 02 Mar 2017 21:16:02 +0100 |
ballarin |
Knaster-Tarski fixed point theorem and Galois Connections.
|
file |
diff |
annotate
|
| Wed, 01 Mar 2017 11:26:19 +0100 |
wenzelm |
more uniform platform settings;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 23:12:52 +0100 |
wenzelm |
more detailed platform information;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 13:51:47 +0000 |
paulson |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 17:17:26 +0000 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 00:00:28 +0100 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 23:50:19 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 13:22:14 +0100 |
haftmann |
re-established AFP entry for FinFuns as library
|
file |
diff |
annotate
|
| Fri, 24 Feb 2017 12:24:13 +0100 |
wenzelm |
avoid Unicode that conflicts with Isabelle symbol rendering;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 20:33:53 +0100 |
haftmann |
more precise NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 20:24:50 +0100 |
haftmann |
basic documentation for computations
|
file |
diff |
annotate
|
| Mon, 13 Feb 2017 16:03:53 +0100 |
fleury |
renaming multiset simprocs
|
file |
diff |
annotate
|
| Sat, 04 Feb 2017 21:15:11 +0100 |
wenzelm |
more uniform use of Reconstruct.clean_proof_of;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 16:11:47 +0100 |
wenzelm |
removed some old ASCII syntax;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2017 15:51:33 +0100 |
wenzelm |
clarified settings;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2017 15:48:26 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 11 Jan 2017 16:43:31 +0100 |
blanchet |
generalized types in lemmas
|
file |
diff |
annotate
|
| Tue, 10 Jan 2017 16:53:05 +0100 |
wenzelm |
support "purge" operation on document model;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 14:40:31 +0000 |
paulson |
Jordan Curve Theorem
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 00:08:18 +0100 |
wenzelm |
NEWS for VSCode;
|
file |
diff |
annotate
|
| Sun, 08 Jan 2017 19:34:44 +0100 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:33 +0100 |
haftmann |
tuned NEWS
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 08:43:30 +0100 |
haftmann |
proper logical constants
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 21:26:26 +0100 |
haftmann |
prefer existing logical constant over abbreviation
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 21:26:26 +0100 |
haftmann |
dropped aliasses
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 22:14:53 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 21:58:13 +0100 |
wenzelm |
added isabelle jedit -R;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 17:40:06 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 12 Dec 2016 11:33:14 +0100 |
wenzelm |
proper session HOL-Types_To_Sets;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2016 17:22:51 +0100 |
bulwahn |
remove typo in bij_swap_compose_bij theorem name; tune proof
|
file |
diff |
annotate
|
| Tue, 29 Nov 2016 08:32:46 +0100 |
blanchet |
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
|
file |
diff |
annotate
|
| Sun, 27 Nov 2016 20:25:38 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 27 Nov 2016 13:19:29 +0100 |
wenzelm |
NEWS for e6a3c55b929b;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2016 11:33:55 +0100 |
haftmann |
clarified NEWS concerning Library/Poly_Deriv
|
file |
diff |
annotate
|
| Sun, 20 Nov 2016 20:12:42 +0100 |
wenzelm |
more on "Formal scopes and semantic selection";
|
file |
diff |
annotate
|
| Thu, 03 Nov 2016 08:10:56 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 03 Nov 2016 08:10:56 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 01 Nov 2016 01:20:33 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 12:14:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 11:55:38 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 22:42:07 +0200 |
blanchet |
added Nunchaku integration
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 13:50:12 +0200 |
eberlm |
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
|
file |
diff |
annotate
|
| Sat, 22 Oct 2016 12:34:58 +0200 |
wenzelm |
regular user tool;
|
file |
diff |
annotate
|
| Thu, 20 Oct 2016 19:39:27 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 16:04:44 +0200 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Wed, 19 Oct 2016 14:43:11 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 19 Oct 2016 14:42:28 +0200 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 18:48:53 +0200 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 19:55:56 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:00:46 +0200 |
wenzelm |
re-use "threads" for --gcthreads;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 22:43:51 +0200 |
wenzelm |
isabelle build -N;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
clarified theorem names
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Mon, 10 Oct 2016 15:45:41 +0100 |
paulson |
invariance of domain
|
file |
diff |
annotate
|
| Sat, 08 Oct 2016 14:09:53 +0200 |
haftmann |
dedicated syntax for types with a length
|
file |
diff |
annotate
|
| Sat, 08 Oct 2016 13:50:25 +0200 |
fleury |
clarifying NEWS file
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 17:58:36 +0200 |
fleury |
tuning multisets
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:45:21 +0200 |
eberlm |
Set_Permutations -> Multiset_Permutations in NEWS
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:31:34 +0200 |
wenzelm |
moved to proper release (cf. 4a72b37ac4b8);
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 10:23:50 +0200 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 14:34:31 +0200 |
haftmann |
option to report results of solve_direct as explicit warnings
|
file |
diff |
annotate
|
| Sun, 02 Oct 2016 17:05:48 +0200 |
wenzelm |
added isabelle_java cold-start executable;
|
file |
diff |
annotate
|
| Sun, 02 Oct 2016 12:29:18 +0200 |
wenzelm |
just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 23:05:25 +0200 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:16:35 +0200 |
wenzelm |
clarified lfp/gfp statements and proofs;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 12:03:27 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 20:54:45 +0200 |
boehmes |
NEWS: new proof method "argo"
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:53 +0200 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 11:25:27 +0200 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 00:12:17 +0200 |
wenzelm |
raw control symbols are superseded by Latex.embed_raw;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 22:43:06 +0200 |
wenzelm |
more general mixfix delimiters;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2016 14:51:58 +0200 |
eberlm |
NEWS: Normalized_Fraction.thy
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 23:14:34 +0200 |
kuncar |
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:07:39 +0200 |
fleury |
# after multiset intersection and union symbol
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 12:53:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 15:16:42 +0200 |
wenzelm |
clarified notation;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 16:33:24 +0200 |
traytel |
NEWS
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 20:57:43 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 14:37:38 +0200 |
wenzelm |
discontinued global etc/abbrevs;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 17:32:09 +0200 |
blanchet |
NEWS
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 18:18:57 +0200 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 22:28:30 +0200 |
wenzelm |
unfold_abs_def is enabled by default;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:39:15 +0200 |
wenzelm |
clarified obscure facts;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
tuning multisets; more interpretations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 10:48:06 +0200 |
blanchet |
added warning
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 16:12:55 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 14:19:27 +0200 |
wenzelm |
uniform ML and document antiquotations;
|
file |
diff |
annotate
|
| 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
|