| 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 |