Changes

#1773 (Jun 27, 2018, 3:26:34 AM)

1. merged — wenzelm / hgweb
2. smart_implode "$AFP" as well; — wenzelm / hgweb
3. merged — paulson / hgweb
4. a few new lemmas — paulson <lp15@cam.ac.uk> / hgweb
5. new theory Trie — nipkow / hgweb

#1772 (Jun 26, 2018, 10:08:52 PM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. updated documentation; — wenzelm / hgweb
4. clarified syntax; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. simplified: allow only command names, with dummy for default; — wenzelm / hgweb
7. clarified: more uniform keyword_tags; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. more flexible document_tags; — wenzelm / hgweb
10. prefer explicit options;
    tuned; — wenzelm / hgweb
11. clarified default tag; — wenzelm / hgweb
12. add URL; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. more explicit statement of rat_denum to fit with top100 thms list — kleing / hgweb

#1771 (Jun 26, 2018, 4:49:05 PM)

1. deleted redundant theorem — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. Rationalisation of complex transcendentals, esp the Arg function — paulson <lp15@cam.ac.uk> / hgweb

#1770 (Jun 26, 2018, 3:25:04 PM)

1. support NUMA shuffling in CI — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1769 (Jun 26, 2018, 11:01:06 AM)

1. merged — wenzelm / hgweb
2. more scalable output; — wenzelm / hgweb

#1768 (Jun 25, 2018, 5:51:45 PM)

1. obsolete — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1767 (Jun 25, 2018, 3:56:41 PM)

1. merged — paulson / hgweb
2. Renaming Arg -> Arg2pi — paulson <lp15@cam.ac.uk> / hgweb

#1766 (Jun 25, 2018, 2:52:05 PM)

1. added lemmas; uniform names — nipkow / hgweb

#1765 (Jun 24, 2018, 10:40:02 PM)

1. disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment; — wenzelm / hgweb

#1764 (Jun 24, 2018, 4:13:06 PM)

1. simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness; — wenzelm / hgweb

#1763 (Jun 24, 2018, 2:13:04 PM)

1. merged — paulson / hgweb
2. more modernisaton and de-applying — paulson <lp15@cam.ac.uk> / hgweb

#1762 (Jun 23, 2018, 5:37:07 PM)

1. tuned; — wenzelm / hgweb
2. clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions; — wenzelm / hgweb

#1761 (Jun 22, 2018, 10:31:07 PM)

1. merged — wenzelm / hgweb
2. clarified document antiquotation @{theory}; — wenzelm / hgweb
3. include target sessions as well: avoid default "Draft" qualification; — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. more uniform syntax; — wenzelm / hgweb
6. more documentation; — wenzelm / hgweb

#1760 (Jun 22, 2018, 1:19:06 AM)

1. merged — paulson / hgweb
2. de-applying Divisibility — paulson <lp15@cam.ac.uk> / hgweb

#1759 (Jun 21, 2018, 12:49:04 PM)

1. more documentation; — wenzelm / hgweb
2. tuned signature -- facilitate testing; — wenzelm / hgweb

#1758 (Jun 21, 2018, 2:17:54 AM)

1. merged — paulson / hgweb
2. More clear-up of Divisibility — paulson <lp15@cam.ac.uk> / hgweb

#1757 (Jun 20, 2018, 11:52:04 PM)

1. updated to polyml-5.7.1-6; — wenzelm / hgweb

#1756 (Jun 20, 2018, 12:01:03 PM)

1. clarified documentation; — wenzelm / hgweb

#1755 (Jun 20, 2018, 10:49:03 AM)

1. merged — paulson / hgweb
2. Partial de-apply of Divisibility — paulson <lp15@cam.ac.uk> / hgweb

#1754 (Jun 19, 2018, 9:10:04 PM)

1. In interpretation commands, clarify what to do with definitions immediately subject to rewriting. — ballarin / hgweb

#1753 (Jun 19, 2018, 3:22:07 PM)

1. merged — paulson / hgweb
2. fixing overloading problems involving vector cross products — paulson <lp15@cam.ac.uk> / hgweb
3. corrections to markup — paulson <lp15@cam.ac.uk> / hgweb
4. New material in support of quaternions — paulson <lp15@cam.ac.uk> / hgweb

#1752 (Jun 19, 2018, 12:40:05 AM)

1. De-applied Ideal.thy — paulson <lp15@cam.ac.uk> / hgweb

#1751 (Jun 18, 2018, 2:37:02 PM)

1. material on finite sets and maps — Lars Hupel <lars.hupel@mytum.de> / hgweb
2. simplify parametricity proofs — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1750 (Jun 18, 2018, 7:34:03 AM)

1. merged — nipkow / hgweb
2. added simp rules — nipkow / hgweb

#1749 (Jun 18, 2018, 12:19:04 AM)

1. merged — paulson / hgweb
2. Algebra tidy-up — paulson <lp15@cam.ac.uk> / hgweb

#1748 (Jun 17, 2018, 3:46:02 PM)

1. added simp rule — nipkow / hgweb

#1747 (Jun 17, 2018, 7:22:04 AM)

1. more simp — nipkow / hgweb
2. moved lemmas from AFP — nipkow / hgweb

#1746 (Jun 16, 2018, 11:16:04 AM)

1. moved lemmas from AFP — nipkow / hgweb

#1745 (Jun 15, 2018, 3:30:13 PM)

1. merged — paulson / hgweb
2. more on infinite products. Also subgroup_imp_subset -> subgroup.subset — paulson <lp15@cam.ac.uk> / hgweb

#1744 (Jun 15, 2018, 2:07:06 PM)

1. empty -> Map.empty — nipkow / hgweb
2. Map.empty now qualified to avoid name clashes — nipkow / hgweb

#1743 (Jun 14, 2018, 6:01:07 PM)

1. auto update; — wenzelm / hgweb
2. merged — paulson / hgweb
3. Adjusting Number_Theory for new Algebra — paulson <lp15@cam.ac.uk> / hgweb
4. merged — paulson / hgweb
5. reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories — paulson <lp15@cam.ac.uk> / hgweb
6. merged — paulson / hgweb
7. New material from Martin Baillon and Paulo Emílio de Vilhena — paulson <lp15@cam.ac.uk> / hgweb

#1742 (Jun 14, 2018, 3:52:06 PM)

1. tuned — nipkow / hgweb

#1741 (Jun 14, 2018, 10:58:05 AM)

1. removed duplicates — nipkow / hgweb

#1740 (Jun 13, 2018, 3:31:02 PM)

1. qualify interpretations to avoid clashes — nipkow / hgweb

#1739 (Jun 13, 2018, 11:53:56 AM)

1. more abstract names — nipkow / hgweb
2. tuned exception — immler / hgweb

#1738 (Jun 13, 2018, 10:52:06 AM)

1. restructured — immler / hgweb
2. result of unoverload is not in normal form — immler / hgweb

#1737 (Jun 13, 2018, 9:31:06 AM)

1. tuned — immler / hgweb
2. allow for a list of vars — immler / hgweb
3. parse var — immler / hgweb

#1736 (Jun 12, 2018, 7:40:03 PM)

1. merged — nipkow / hgweb
2. more abstract naming — nipkow / hgweb
3. tuned — immler / hgweb
4. workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar — immler / hgweb

#1735 (Jun 12, 2018, 4:40:02 PM)

1. a derived rule combining unoverload and internalize_sort — immler / hgweb

#1734 (Jun 12, 2018, 1:43:05 PM)

1. merged — paulson / hgweb
2. fixed a name clash — paulson <lp15@cam.ac.uk> / hgweb
3. merged — paulson / hgweb
4. the last of the infinite product proofs — paulson <lp15@cam.ac.uk> / hgweb

#1733 (Jun 12, 2018, 7:25:04 AM)

1. merged — nipkow / hgweb
2. proved avl for map (finally); tuned — nipkow / hgweb

#1732 (Jun 12, 2018, 12:55:06 AM)

1. merged — paulson / hgweb
2. tidier Cauchy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1731 (Jun 11, 2018, 10:49:50 PM)

1. merged — wenzelm / hgweb
2. more abstract Export.Provider; — wenzelm / hgweb
3. clarified signature: persistent results; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned def. of del and proved preservation of rbt (finally) — nipkow / hgweb

#1730 (Jun 11, 2018, 7:13:09 PM)

1. merged — nipkow / hgweb
2. tuned order of arguments — nipkow / hgweb

#1729 (Jun 11, 2018, 3:43:03 PM)

1. default value for parametricity of dim — immler / hgweb

#1728 (Jun 11, 2018, 8:22:06 AM)

1. added lemma — nipkow / hgweb

#1727 (Jun 9, 2018, 10:04:05 PM)

1. clarified signature: more uniform theory_message (see also d7920eb7de54); — wenzelm / hgweb

#1726 (Jun 9, 2018, 1:31:08 PM)

1. tuned -- use existing operation; — wenzelm / hgweb

#1725 (Jun 7, 2018, 11:43:03 PM)

1. merged — wenzelm / hgweb
2. isabelle emacs no longer exists; — wenzelm / hgweb

#1724 (Jun 7, 2018, 7:43:08 PM)

1. utilize 'flip' — nipkow / hgweb

#1723 (Jun 7, 2018, 3:16:07 PM)

1. comments — nipkow / hgweb

#1722 (Jun 6, 2018, 7:00:13 PM)

1. merged — nipkow / hgweb
2. reorient -> split; documented split — nipkow / hgweb
3. merged — wenzelm / hgweb
4. Added tag Isabelle2018-RC0 for changeset 194fa3d2d6a4 — wenzelm / hgweb
5. merged — paulson / hgweb
6. resolution of name clashes in Algebra — paulson <lp15@cam.ac.uk> / hgweb

#1721 (Jun 6, 2018, 3:39:47 PM)

1. merged — wenzelm / hgweb
2. isabelle update_comments; — wenzelm / hgweb
3. tuned header; — wenzelm / hgweb
4. updated for release; — wenzelm / hgweb
5. updated for release; — wenzelm / hgweb
6. misc tuning and updates for release; — wenzelm / hgweb
7. updated for release; — wenzelm / hgweb
8. updated for release;
   tuned; — wenzelm / hgweb
9. eliminated suspicious Unicode; — wenzelm / hgweb
10. proper white space; — wenzelm / hgweb
11. updated to sqlite-jdbc-3.23.1; — wenzelm / hgweb

#1720 (Jun 6, 2018, 1:10:07 PM)

1. merged — nipkow / hgweb
2. Keep filter input syntax — nipkow / hgweb

#1719 (Jun 6, 2018, 12:48:25 AM)

1. more parallelism to cope with 8h30 CPU time; — wenzelm / hgweb

#1718 (Jun 5, 2018, 11:10:04 PM)

1. full benchmarks, including all conditional theories; — wenzelm / hgweb

#1717 (Jun 5, 2018, 6:49:08 PM)

1. tuned proofs; — wenzelm / hgweb

#1716 (Jun 5, 2018, 4:55:03 PM)

1. more robust; — wenzelm / hgweb
2. less wasteful consolidation, based on PIDE front-end state and recent changes; — wenzelm / hgweb
3. tuned -- short-circuit result; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb

#1715 (Jun 5, 2018, 1:07:45 AM)

1. updated URLs; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. more robust; — wenzelm / hgweb
4. avoid hardwired cygwin mirror; — wenzelm / hgweb
5. updated to current Cygwin, after 2.10.0-1 from 02-Feb-2018;
   record cygwin mirror explicitly; — wenzelm / hgweb

#1714 (Jun 4, 2018, 11:40:05 PM)

1. NEWS: infinite products — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. more tweaks of Cauchy — paulson <lp15@cam.ac.uk> / hgweb

#1713 (Jun 4, 2018, 2:31:04 PM)

1. clarified signature;
   simplified options; — wenzelm / hgweb

#1712 (Jun 4, 2018, 1:23:41 AM)

1. tuned proofs; — wenzelm / hgweb

#1711 (Jun 3, 2018, 10:46:05 PM)

1. NEWS; — wenzelm / hgweb
2. proper function invocation with all arguments; — wenzelm / hgweb
3. fork parallel prints early in execution: avoid degradation of priority due to main eval task; — wenzelm / hgweb
4. clarified signature: prefer Document.Snapshot; — wenzelm / hgweb

#1710 (Jun 3, 2018, 7:58:40 PM)

1. list syntax details — nipkow / hgweb
2. merged — nipkow / hgweb
3. allow tuple patterns in list comprehensions — nipkow / hgweb

#1709 (Jun 3, 2018, 5:37:04 PM)

1. infinite product material — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. tidied more Cauchy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1708 (Jun 2, 2018, 10:49:05 PM)

1. tuned proofs; — wenzelm / hgweb
2. more symbols; — wenzelm / hgweb
3. more formal comments; — wenzelm / hgweb
4. more args; — wenzelm / hgweb
5. record active execution task and depend on it -- avoid new executions bumping into old ones; — wenzelm / hgweb
6. tuned -- more explicit types; — wenzelm / hgweb
7. less frequent consolidation: it requires a full Document.update and Document.start_execution; — wenzelm / hgweb

#1707 (Jun 1, 2018, 11:28:07 PM)

1. varify frees, notably dangling_params (see also e0cd57aeb60c); — wenzelm / hgweb
2. tuned -- more explicit expression; — wenzelm / hgweb

#1706 (Jun 1, 2018, 4:25:06 PM)

1. merged — wenzelm / hgweb
2. documentation for "isabelle dump"; — wenzelm / hgweb
3. more dump aspects, with options;
   tuned signature; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. clarified default: all aspects; — wenzelm / hgweb
6. clarified priority; — wenzelm / hgweb

#1705 (Jun 1, 2018, 1:40:05 PM)

1. merged — nipkow / hgweb
2. added lemma — nipkow / hgweb

#1704 (Jun 1, 2018, 12:22:05 PM)

1. Fixed latex markup — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. more tidying — paulson <lp15@cam.ac.uk> / hgweb

#1703 (May 31, 2018, 11:25:06 PM)

1. merged — wenzelm / hgweb
2. more symbols; — wenzelm / hgweb
3. Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
   tuned; — wenzelm / hgweb
4. clarified: consolidated result is last command; — wenzelm / hgweb
5. support for anonymous print function values;
   clarified treatment of retained_prints; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. store Isabelle symbols in canonical form;
   tuned signature; — wenzelm / hgweb
8. clarified outermost progress.interrupt_handler; — wenzelm / hgweb
9. report theory progress via PIDE node status; — wenzelm / hgweb

#1702 (May 31, 2018, 11:01:05 AM)

1. merge — blanchet / hgweb
2. more conservative output, avoiding nonstandard feature of E — blanchet / hgweb
3. merged — paulson / hgweb
4. winding numbers predicate — paulson <lp15@cam.ac.uk> / hgweb

#1701 (May 30, 2018, 1:52:05 PM)

1. unused — nipkow / hgweb

#1700 (May 29, 2018, 10:58:03 PM)

1. merged — wenzelm / hgweb
2. more node status information; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. shutdown ML process before output: Theories_Result is timeless/stateless; — wenzelm / hgweb
6. more operations;
   more output; — wenzelm / hgweb
7. more accurate dependencies;
   tuned; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. more formal dump aspects;
   support output dir; — wenzelm / hgweb
10. more operations (as in ML); — wenzelm / hgweb
11. clarified option -O: avoid conflict with build/dump option -D; — wenzelm / hgweb

#1699 (May 29, 2018, 8:07:07 PM)

1. slicker proof — nipkow / hgweb

#1698 (May 29, 2018, 3:19:06 PM)

1. canonical names — nipkow / hgweb

#1697 (May 29, 2018, 10:01:04 AM)

1. merged — paulson / hgweb
2. more general tidying — paulson <lp15@cam.ac.uk> / hgweb

#1696 (May 28, 2018, 10:46:06 PM)

1. merged — wenzelm / hgweb
2. support to dump build database produced by PIDE session; — wenzelm / hgweb
3. more accurate theory_graph: avoid imports of loaded_theories with incomplete node name; — wenzelm / hgweb
4. clarified signature: Known.theories retains Document.Node.Entry (with header); — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb

#1695 (May 28, 2018, 10:49:02 AM)

1. merged — paulson / hgweb
2. tidying up a bit more — paulson <lp15@cam.ac.uk> / hgweb

#1694 (May 27, 2018, 11:47:29 PM)

1. prefer existing operation; — wenzelm / hgweb

#1693 (May 27, 2018, 10:49:04 PM)

1. retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later; — wenzelm / hgweb
2. clarified signature -- avoid confusion with Resources.is_hidden; — wenzelm / hgweb

#1691 (May 27, 2018, 12:43:05 AM)

1. merged — paulson / hgweb
2. tidying and reorganisation around Cauchy Integral Theorem — paulson <lp15@cam.ac.uk> / hgweb

#1690 (May 26, 2018, 10:31:04 PM)

1. export sort algebra; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. support 'export_files' in session ROOT; — wenzelm / hgweb
5. clarified output; — wenzelm / hgweb
6. support multiple patterns; — wenzelm / hgweb
7. clarified cache; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. tuned output; — wenzelm / hgweb

#1689 (May 26, 2018, 1:16:27 PM)

1. merged — paulson / hgweb
2. merged — paulson / hgweb
3. tidied some proofs — paulson <lp15@cam.ac.uk> / hgweb
4. merged — paulson / hgweb
5. merged — paulson / hgweb
6. more small tidying — paulson <lp15@cam.ac.uk> / hgweb

#1688 (May 26, 2018, 11:13:02 AM)

1. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
2. macOS build: exclude HOL-Proofs — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1687 (May 25, 2018, 11:34:05 PM)

1. tuned; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. added command 'ML_export'; — wenzelm / hgweb
4. more examples; — wenzelm / hgweb
5. tuned output; — wenzelm / hgweb
6. pretty-print according to defaults of input syntax; — wenzelm / hgweb
7. more accurate diagram; — wenzelm / hgweb
8. proper output; — wenzelm / hgweb

#1686 (May 25, 2018, 6:34:03 PM)

1. treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd — haftmann / hgweb

#1685 (May 25, 2018, 1:41:09 AM)

1. merged — wenzelm / hgweb
2. setup server directory for Cygwin quasi-mirror; — wenzelm / hgweb
3. more scalable JVM memory management; — wenzelm / hgweb
4. tuned output; — wenzelm / hgweb
5. more general cache, also for term substructures; — wenzelm / hgweb
6. more exports;
   read_session: proper signature; — wenzelm / hgweb

#1684 (May 24, 2018, 7:19:38 PM)

1. generalized Cramer's rule — immler / hgweb

#1683 (May 24, 2018, 4:46:06 PM)

1. tuned — nipkow / hgweb

#1682 (May 24, 2018, 3:05:18 PM)

1. reorganization, everything based on Tree2 now — nipkow / hgweb

#1681 (May 24, 2018, 9:59:57 AM)

1. avoid overaggressive classical rule — haftmann / hgweb

#1680 (May 24, 2018, 8:07:06 AM)

1. By Andrei Popescu based on an initial version by Kasper F. Brandt — nipkow / hgweb

#1679 (May 24, 2018, 12:28:05 AM)

1. merged — paulson / hgweb
2. small tidy-up of Complex_Transcendental — paulson <lp15@cam.ac.uk> / hgweb
3. merged — paulson / hgweb
4. small clean-up of Complex_Analysis_Basics — paulson <lp15@cam.ac.uk> / hgweb

#1678 (May 23, 2018, 12:45:38 PM)

1. more complete and more correct documentation on code generation — haftmann / hgweb
2. grouped material on numeral division — haftmann / hgweb

#1677 (May 23, 2018, 9:16:06 AM)

1. automatic classical rule to derive a dvd b from b mod a = 0 — haftmann / hgweb
2. consider dvdE for automated classical proving — haftmann / hgweb

#1676 (May 22, 2018, 6:22:53 PM)

1. added lambda-free HO output for Ehoh (higher-order E prototype) — blanchet / hgweb

#1675 (May 22, 2018, 4:31:07 PM)

1. First step to remove nonstandard "[x <- xs. P]" syntax: only input — nipkow / hgweb
2. merged — nipkow / hgweb
3. removed unicode symbol — nipkow / hgweb
4. Moved Landau_Symbols from the AFP to HOL-Library — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1674 (May 22, 2018, 11:25:06 AM)

1. merged — wenzelm / hgweb
2. more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact); — wenzelm / hgweb

#1673 (May 21, 2018, 6:43:03 PM)

1. no longer necessary — nipkow / hgweb

#1672 (May 21, 2018, 1:01:03 AM)

1. merged — paulson / hgweb
2. correcting the statements of the MVTs — paulson <lp15@cam.ac.uk> / hgweb
3. one last fix — paulson <lp15@cam.ac.uk> / hgweb
4. tidy up of Derivative — paulson <lp15@cam.ac.uk> / hgweb

#1671 (May 20, 2018, 10:49:03 PM)

1. avoid undeclared frees; — wenzelm / hgweb
2. removed junk; — wenzelm / hgweb
3. avoid dangling tfrees; — wenzelm / hgweb
4. standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. avoid undeclared frees; — wenzelm / hgweb
7. export facts; — wenzelm / hgweb
8. clarified encoding; — wenzelm / hgweb
9. more scalable; — wenzelm / hgweb
10. tuned output; — wenzelm / hgweb
11. more scalable; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. support HTTPS; — wenzelm / hgweb
14. updated to scala-2.12.6; — wenzelm / hgweb
15. prefer HTTPS; — wenzelm / hgweb

#1670 (May 19, 2018, 9:49:04 PM)

1. override default of Isabelle_Process, notably for PIDE export of "document.tex"; — wenzelm / hgweb
2. tuned queries; — wenzelm / hgweb
3. support for build_database_server (PostgreSQL);
   clarified signature; — wenzelm / hgweb
4. clarified store.clean_output: cleanup user_output_dir even in system_mode; — wenzelm / hgweb
5. clarified store directories;
   discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. clarified handling of output heap; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb

#1669 (May 19, 2018, 12:04:07 PM)

1. added lemmas — nipkow / hgweb

#1668 (May 18, 2018, 10:40:05 PM)

1. more abstract database access; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. clarified heap vs. database operations: discontinued correlation of directory; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. support Store with options; — wenzelm / hgweb
7. more exports; — wenzelm / hgweb

#1667 (May 17, 2018, 8:20:00 PM)

1. updated some Sledgehammer components, following Makarius advice — blanchet / hgweb

#1666 (May 17, 2018, 6:26:50 PM)

1. export more theory and session structure; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb

#1665 (May 17, 2018, 4:34:04 PM)

1. clarified signature; — wenzelm / hgweb
2. read theory content from session database; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. misc tuning and clarification; — wenzelm / hgweb

#1664 (May 17, 2018, 7:49:02 AM)

1. NEWS and CONTRIBUTORS for 8b50f29a1992 — Andreas Lochbihler / hgweb

#1663 (May 17, 2018, 12:42:16 AM)

1. proper PIDE positions; — wenzelm / hgweb

#1662 (May 16, 2018, 10:49:06 PM)

1. avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout); — wenzelm / hgweb
2. clarified "consolidation" vs. "presentation"; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb

#1661 (May 16, 2018, 5:37:05 PM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more thorough checks for theory name consistency (for extend, not just merge); — wenzelm / hgweb
4. more uniform output (cf. 450cefec7c11); — wenzelm / hgweb

#1660 (May 16, 2018, 6:16:03 AM)

1. removed duplicates — nipkow / hgweb
2. added lemmas — nipkow / hgweb

#1659 (May 15, 2018, 3:08:15 PM)

1. tuned headers; — wenzelm / hgweb

#1658 (May 15, 2018, 11:46:04 AM)

1. move FuncSet back to HOL-Library (amending 493b818e8e10) — immler / hgweb

#1657 (May 15, 2018, 6:31:03 AM)

1. merged — nipkow / hgweb
2. cleaning up sorted — nipkow / hgweb

#1656 (May 14, 2018, 11:19:07 PM)

1. merged — wenzelm / hgweb
2. support for dynamic document output while editing; — wenzelm / hgweb
3. adjust position according to offset of command/exec id; — wenzelm / hgweb
4. tuned signature (see Command.eval_state); — wenzelm / hgweb
5. export generated document.tex, unless explicit document=false; — wenzelm / hgweb
6. more general presentation hook, with document preparation as application; — wenzelm / hgweb
7. clarified signature: more explicit type "context" with full options; — wenzelm / hgweb
8. more explicit type Thy_Output.segment; — wenzelm / hgweb
9. clarified signature;
   more operations; — wenzelm / hgweb

#1655 (May 14, 2018, 6:25:06 PM)

1. more sorted cleaning — nipkow / hgweb
2. cleaning up sorted — nipkow / hgweb

#1654 (May 13, 2018, 10:43:03 PM)

1. merged — wenzelm / hgweb
2. more uniform types vs. consts; — wenzelm / hgweb
3. more concise information; — wenzelm / hgweb
4. export foundational theory content in Scala; — wenzelm / hgweb
5. clarified markup; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. tuned -- use XZ.Cache; — wenzelm / hgweb
8. clarified implicit compression; — wenzelm / hgweb
9. tuned -- use XZ.Cache; — wenzelm / hgweb
10. more exports;
    misc tuning and clarification; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more operations; — wenzelm / hgweb

#1653 (May 13, 2018, 4:00:02 PM)

1. tuned — nipkow / hgweb
2. tuned — nipkow / hgweb

#1652 (May 13, 2018, 2:09:17 PM)

1. mv lemma — nipkow / hgweb
2. removed unused lemma — nipkow / hgweb

#1651 (May 13, 2018, 1:13:02 PM)

1. tuned — nipkow / hgweb

#1650 (May 13, 2018, 8:13:06 AM)

1. removed some non-essential rules — haftmann / hgweb

#1649 (May 12, 2018, 6:01:03 PM)

1. added lemmas — nipkow / hgweb

#1648 (May 12, 2018, 1:34:03 PM)

1. new tool Code_Lazy — Andreas Lochbihler / hgweb

#1647 (May 11, 2018, 11:25:06 PM)

1. some export of foundational theory content; — wenzelm / hgweb
2. support for general theory presentation; — wenzelm / hgweb

#1646 (May 11, 2018, 9:13:05 PM)

1. guard result exports via export_pattern -- avoid bombing client via huge blobs; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. clarified output: avoid costly operations on huge blobs; — wenzelm / hgweb
4. unused; — wenzelm / hgweb
5. more scalable -- avoid huge lines within stdout; — wenzelm / hgweb
6. slightly more ambitious parallelism (again); — wenzelm / hgweb
7. more scalable API; — wenzelm / hgweb

#1645 (May 11, 2018, 6:13:04 PM)

1. proper heading; — wenzelm / hgweb
2. removed unused Java FX modules (it will be unbundled from JDK eventually); — wenzelm / hgweb

#1644 (May 11, 2018, 2:29:11 AM)

1. tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1643 (May 10, 2018, 10:26:30 PM)

1. merged — nipkow / hgweb
2. more lemmas — nipkow / hgweb
3. merged — nipkow / hgweb
4. simpler types — nipkow / hgweb

#1642 (May 10, 2018, 6:13:04 PM)

1. auto-tidying — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. more on infinite products — paulson <lp15@cam.ac.uk> / hgweb

#1641 (May 10, 2018, 3:22:11 AM)

1. merged — paulson / hgweb
2. part tidy-up of Determinants — paulson <lp15@cam.ac.uk> / hgweb

#1640 (May 9, 2018, 11:22:05 PM)

1. less ambitious parallelism, notably for threads=2; — wenzelm / hgweb
2. more informative error, notably for missing executable; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. clarified future scheduling parameters, with support for parallel_limit; — wenzelm / hgweb
5. record total number of tasks; — wenzelm / hgweb

#1639 (May 9, 2018, 8:09:44 PM)

1. merged — paulson / hgweb
2. more infinite product theorems — paulson <lp15@cam.ac.uk> / hgweb

#1638 (May 9, 2018, 3:40:02 PM)

1. proper merge of items without term index (amending b969263fcf02); — wenzelm / hgweb

#1637 (May 9, 2018, 10:22:06 AM)

1. announce sorted changes — nipkow / hgweb

#1636 (May 9, 2018, 1:08:03 AM)

1. merged — paulson / hgweb
2. one tiny fix — paulson <lp15@cam.ac.uk> / hgweb
3. merged — paulson / hgweb
4. merged — paulson / hgweb
5. tidying more messy proofs — paulson <lp15@cam.ac.uk> / hgweb
6. merged — nipkow / hgweb
7. more efficient code — nipkow / hgweb

#1635 (May 8, 2018, 9:25:03 PM)

1. merged — wenzelm / hgweb
2. command-line tool "isabelle export";
   more documentation;
   tuned; — wenzelm / hgweb
3. more efficient query; — wenzelm / hgweb
4. more robust: self-export only; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb

#1634 (May 8, 2018, 3:13:06 PM)

1. merged — nipkow / hgweb
2. more "sorted" changes — nipkow / hgweb
3. more "sorted" changes — nipkow / hgweb
4. new def of sorted and sorted_wrt — nipkow / hgweb

#1633 (May 8, 2018, 1:30:59 AM)

1. more operations; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. return exports as result for Isabelle server; — wenzelm / hgweb
4. more checks; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
   tuned; — wenzelm / hgweb
7. clarified signature;
   avoid pointless compression; — wenzelm / hgweb
8. store exports within PIDE command state;
   Markup.Export.unapply: proper NAME; — wenzelm / hgweb

#1632 (May 7, 2018, 10:04:03 PM)

1. removed some lemma duplicates — haftmann / hgweb
2. typo — haftmann / hgweb
3. more appropriate notion of emptiness — haftmann / hgweb

#1631 (May 7, 2018, 11:13:06 AM)

1. merged — paulson / hgweb
2. more tidying — paulson <lp15@cam.ac.uk> / hgweb
3. starting to tidy up Interval_Integral.thy — paulson <lp15@cam.ac.uk> / hgweb

#1630 (May 7, 2018, 1:23:44 AM)

1. more operations; — wenzelm / hgweb

#1629 (May 6, 2018, 11:31:03 PM)

1. merged — wenzelm / hgweb
2. store exports in session database, with asynchronous / parallel compression; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned signature;
   clarified modules; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. protocol message for export of theory resources; — wenzelm / hgweb
7. hexadecimal representation of byte string; — wenzelm / hgweb
8. cleanup session output before starting build job;
   tuned signature; — wenzelm / hgweb

#1628 (May 6, 2018, 5:02:37 PM)

1. reinstated old lemma name — nipkow / hgweb

#1627 (May 6, 2018, 3:04:06 PM)

1. updated to lemma name change — nipkow / hgweb
2. removed asm "finite" — nipkow / hgweb

#1626 (May 4, 2018, 11:10:06 PM)

1. merged — wenzelm / hgweb
2. no censorship of view title; — wenzelm / hgweb
3. set view title dynamically; — wenzelm / hgweb

#1625 (May 4, 2018, 6:49:05 PM)

1. tuned — nipkow / hgweb

#1624 (May 4, 2018, 4:07:04 PM)

1. tuned — nipkow / hgweb

#1623 (May 4, 2018, 12:52:06 AM)

1. Some tidying up (mostly regarding summations from 0) — paulson <lp15@cam.ac.uk> / hgweb
2. tidied up Infinite_Products — paulson <lp15@cam.ac.uk> / hgweb

#1622 (May 3, 2018, 9:22:50 PM)

1. merged — immler / hgweb
2. fixed HOL-Analysis — immler / hgweb
3. merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space) — immler / hgweb
4. added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly — immler / hgweb

#1621 (May 3, 2018, 6:16:03 PM)

1. a lemma about infinite products — paulson <lp15@cam.ac.uk> / hgweb

#1620 (May 3, 2018, 10:58:06 AM)

1. merged — paulson / hgweb
2. tidying up and using real induction methods — paulson <lp15@cam.ac.uk> / hgweb

#1619 (May 3, 2018, 12:22:05 AM)

1. tuned -- slightly smaller future closure size; — wenzelm / hgweb

#1618 (May 2, 2018, 7:28:04 PM)

1. clarified menu actions; — wenzelm / hgweb
2. purge history more thoroughly (see also 3156faac30a7); — wenzelm / hgweb

#1617 (May 2, 2018, 3:13:03 PM)

1. merged — paulson / hgweb
2. type class generalisations; some work on infinite products — paulson <lp15@cam.ac.uk> / hgweb

#1616 (May 2, 2018, 11:04:06 AM)

1. merged — paulson / hgweb
2. simplified some messy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1615 (May 2, 2018, 2:10:04 AM)

1. clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
   tuned headers; — wenzelm / hgweb

#1614 (May 1, 2018, 4:52:03 PM)

1. avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted"; — wenzelm / hgweb

#1613 (May 1, 2018, 12:22:05 AM)

1. merged — paulson / hgweb
2. more general tidying up — paulson <lp15@cam.ac.uk> / hgweb

#1612 (Apr 30, 2018, 8:58:06 AM)

1. prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas — boehmes / hgweb

#1611 (Apr 29, 2018, 11:31:04 PM)

1. cleaned up more messy proofs — paulson <lp15@cam.ac.uk> / hgweb
2. more defer/prefer — paulson <lp15@cam.ac.uk> / hgweb

#1610 (Apr 28, 2018, 11:43:06 PM)

1. getting rid of more "defer", etc. — paulson <lp15@cam.ac.uk> / hgweb

#1609 (Apr 28, 2018, 4:55:04 PM)

1. getting rid of "defer" — paulson <lp15@cam.ac.uk> / hgweb

#1608 (Apr 28, 2018, 12:07:06 AM)

1. another big cleanup — paulson <lp15@cam.ac.uk> / hgweb

#1607 (Apr 27, 2018, 3:55:04 PM)

1. merged — paulson / hgweb
2. minor typeclass generalisations and junk removal — paulson <lp15@cam.ac.uk> / hgweb

#1606 (Apr 27, 2018, 11:07:03 AM)

1. merged — paulson / hgweb
2. more messy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1605 (Apr 26, 2018, 10:04:05 PM)

1. merged — nipkow / hgweb
2. new simp modifier: reorient — nipkow / hgweb

#1604 (Apr 26, 2018, 6:16:05 PM)

1. small typeclass generalisations — paulson <lp15@cam.ac.uk> / hgweb

#1603 (Apr 26, 2018, 3:46:34 PM)

1. merged — paulson / hgweb
2. some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous — paulson <lp15@cam.ac.uk> / hgweb

#1602 (Apr 26, 2018, 2:13:03 PM)

1. spelling; — wenzelm / hgweb

#1601 (Apr 25, 2018, 11:40:05 PM)

1. more messy proofs redone, and new material — paulson <lp15@cam.ac.uk> / hgweb

#1600 (Apr 25, 2018, 8:38:09 PM)

1. merged — paulson / hgweb
2. merged — paulson / hgweb
3. new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP) — paulson <lp15@cam.ac.uk> / hgweb

#1599 (Apr 25, 2018, 5:13:33 PM)

1. merged — wenzelm / hgweb
2. tuned -- avoid spurious exception trace for "the"; — wenzelm / hgweb
3. proof of concept for residue rings over int using type numerals — haftmann / hgweb

#1598 (Apr 25, 2018, 3:22:07 PM)

1. more correct error message — haftmann / hgweb
2. uniform tagging for printable and non-printable literals — haftmann / hgweb

#1597 (Apr 25, 2018, 12:28:04 AM)

1. merged — paulson / hgweb
2. fixing more messy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1596 (Apr 24, 2018, 8:37:03 PM)

1. more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0; — wenzelm / hgweb
2. eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723); — wenzelm / hgweb

#1595 (Apr 24, 2018, 4:34:08 PM)

1. proper datatype for 8-bit characters — haftmann / hgweb
2. corrected nonsense — haftmann / hgweb

#1594 (Apr 24, 2018, 11:46:02 AM)

1. less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap); — wenzelm / hgweb
2. clarified modules; — wenzelm / hgweb

#1593 (Apr 24, 2018, 12:28:05 AM)

1. tidied some horrid proofs — paulson <lp15@cam.ac.uk> / hgweb

#1592 (Apr 23, 2018, 8:16:02 AM)

1. del_max -> split_max — nipkow / hgweb

#1591 (Apr 22, 2018, 11:10:06 PM)

1. Tidied a lot of messy proofs — paulson <lp15@cam.ac.uk> / hgweb

#1590 (Apr 21, 2018, 11:19:04 AM)

1. dont rename PQ.del_min — nipkow / hgweb

#1589 (Apr 21, 2018, 8:49:03 AM)

1. del_min -> split_min — nipkow / hgweb

#1588 (Apr 20, 2018, 11:06:31 PM)

1. merged — wenzelm / hgweb
2. support for XZ.Cache; — wenzelm / hgweb

#1587 (Apr 20, 2018, 9:31:06 PM)

1. three new theorems — paulson <lp15@cam.ac.uk> / hgweb

#1586 (Apr 20, 2018, 4:30:25 PM)

1. merged — wenzelm / hgweb
2. updated to postgresql-42.2.2, with more smooth support for Java 9/10; — wenzelm / hgweb
3. minimal Java source version for jdk-10.0.1; — wenzelm / hgweb
4. workaround for jdk-10.0.1; — wenzelm / hgweb
5. more robust, notably for jdk-10.0.1 where jre is absent; — wenzelm / hgweb

#1585 (Apr 20, 2018, 2:40:04 PM)

1. moved lemma to more appropriate place — haftmann / hgweb
2. algebraic embeddings for bit operations — haftmann / hgweb

#1584 (Apr 19, 2018, 10:58:12 PM)

1. updated to jdk-8u172; — wenzelm / hgweb

#1583 (Apr 19, 2018, 9:52:02 PM)

1. merged — wenzelm / hgweb
2. updated to jfreechart-1.5.0, but retain bundled iText-2.1.5.jar from jfreechart-1.0.14 to avoid iText-5/7 license complexity; — wenzelm / hgweb

#1582 (Apr 19, 2018, 5:13:06 PM)

1. tuning of a proof — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. some simpler, cleaner proofs — paulson <lp15@cam.ac.uk> / hgweb

#1581 (Apr 19, 2018, 2:37:05 PM)

1. prefer explicit 32/64 bit platform settings; — wenzelm / hgweb
2. misc tuning and clarification; — wenzelm / hgweb

#1580 (Apr 18, 2018, 11:34:02 PM)

1. correction of TeX errors and other oversights — paulson <lp15@cam.ac.uk> / hgweb
2. Oops! Change_Of_Vars was not being imported to Analysis! — paulson <lp15@cam.ac.uk> / hgweb

#1579 (Apr 18, 2018, 6:13:05 PM)

1. tidying up including contributions from Paulo Emílio de Vilhena — paulson <lp15@cam.ac.uk> / hgweb

#1578 (Apr 18, 2018, 12:52:02 AM)

1. Change of variables proof — paulson <lp15@cam.ac.uk> / hgweb

#1577 (Apr 17, 2018, 8:04:06 PM)

1. merged — paulson / hgweb
2. Vitali covering theorem — paulson <lp15@cam.ac.uk> / hgweb

#1576 (Apr 17, 2018, 5:43:06 PM)

1. updated to xz-java-1.8; — wenzelm / hgweb
2. updated windows_app to launch4j 3.11 and 7zsd_extra_171_3901.7z (reconstructed by Chris Lake); — wenzelm / hgweb

#1575 (Apr 17, 2018, 4:10:05 PM)

1. NEWS; — wenzelm / hgweb
2. updated to jedit-5.5.0;
   discontinued jedit_build/contrib/jEdit-patched.tar.gz -- its content is in directory jedit_build/contrib/jedit-5.5.0-patched/jEdit; — wenzelm / hgweb

#1574 (Apr 17, 2018, 12:37:04 PM)

1. more about measure — paulson <lp15@cam.ac.uk> / hgweb

#1573 (Apr 16, 2018, 11:43:05 PM)

1. some more random results — paulson <lp15@cam.ac.uk> / hgweb

#1572 (Apr 16, 2018, 5:07:04 PM)

1. more results about measure and negligibility — paulson <lp15@cam.ac.uk> / hgweb

#1571 (Apr 16, 2018, 10:10:03 AM)

1. explicit simp rules for computing abstract bit operations — haftmann / hgweb

#1570 (Apr 16, 2018, 7:40:07 AM)

1. more and generalized lemmas — haftmann / hgweb

#1569 (Apr 15, 2018, 11:52:05 PM)

1. quite a few more results about negligibility, etc., and a bit of tidying up — paulson <lp15@cam.ac.uk> / hgweb

#1568 (Apr 15, 2018, 7:49:04 PM)

1. merged — paulson / hgweb
2. a few more results — paulson <lp15@cam.ac.uk> / hgweb

#1567 (Apr 15, 2018, 5:55:03 PM)

1. added bottom-up merge sort — nipkow / hgweb

#1566 (Apr 15, 2018, 4:10:03 PM)

1. various new results on measures, integrals, etc., and some simplified proofs — paulson <lp15@cam.ac.uk> / hgweb

#1565 (Apr 14, 2018, 10:31:04 PM)

1. more new theorems on real^1, matrices, etc. — paulson <lp15@cam.ac.uk> / hgweb

#1564 (Apr 14, 2018, 5:58:03 PM)

1. a few new theorems and some fixes — paulson <lp15@cam.ac.uk> / hgweb

#1563 (Apr 14, 2018, 1:31:03 PM)

1. new material about vec, real^1, etc. — paulson <lp15@cam.ac.uk> / hgweb

#1562 (Apr 13, 2018, 8:28:34 PM)

1. merged — paulson / hgweb
2. Probability builds with new definitions — paulson <lp15@cam.ac.uk> / hgweb
3. Analysis builds using set_borel_measurable_def, etc. — paulson <lp15@cam.ac.uk> / hgweb
4. merged — paulson / hgweb
5. replacement of set integral abbreviations by actual definitions! — paulson <lp15@cam.ac.uk> / hgweb

#1561 (Apr 13, 2018, 5:31:03 PM)

1. added lemma — nipkow / hgweb

#1560 (Apr 11, 2018, 11:07:07 AM)

1. avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle — boehmes / hgweb

#1559 (Apr 10, 2018, 11:55:05 AM)

1. merged — paulson / hgweb
2. A couple of new results — paulson <lp15@cam.ac.uk> / hgweb
3. Syntax for the special cases Min(A`I) and Max (A`I) — paulson <lp15@cam.ac.uk> / hgweb

#1558 (Apr 9, 2018, 4:28:06 PM)

1. removed dots at the end of (sub)titles — nipkow / hgweb

#1557 (Apr 8, 2018, 12:40:07 PM)

1. moved and renamed lemmas — nipkow / hgweb
2. Added binary set operations with join-based implementation — nipkow / hgweb
3. more name tuning — nipkow / hgweb
4. better name; added binary operations — nipkow / hgweb

#1556 (Apr 7, 2018, 10:16:04 PM)

1. tuned — nipkow / hgweb

#1555 (Apr 6, 2018, 6:25:06 PM)

1. a first shot at tagging for HOL-Analysis manual — immler / hgweb

#1554 (Apr 5, 2018, 5:46:07 PM)

1. even more on bit operations — haftmann / hgweb

#1553 (Apr 5, 2018, 8:16:08 AM)

1. more bit operation conversions — haftmann / hgweb

#1552 (Apr 4, 2018, 7:58:03 PM)

1. more rules for numeral conversions;
   more precise code setup for pred_numeral — haftmann / hgweb

#1551 (Mar 28, 2018, 11:04:04 PM)

1. tuned proofs and generalized some lemmas about limits — huffman / hgweb
2. tuned some proofs — huffman / hgweb
3. tuned some proofs about filters — huffman / hgweb

#1550 (Mar 28, 2018, 1:55:02 PM)

1. clarified handling of stdout vs. stderr: the cronjob should normally be silent; — wenzelm / hgweb

#1549 (Mar 28, 2018, 12:01:07 PM)

1. proper self_update of components -- do assume shared file-system; — wenzelm / hgweb

#1548 (Mar 27, 2018, 2:46:05 PM)

1. updated to scala-2.12.5; — wenzelm / hgweb

#1547 (Mar 27, 2018, 12:07:07 AM)

1. Merged — Manuel Eberl <eberlm@in.tum.de> / hgweb
2. Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa) — Manuel Eberl <eberlm@in.tum.de> / hgweb
3. Added some simple facts about limits — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1546 (Mar 26, 2018, 9:04:05 PM)

1. added lemmas — nipkow / hgweb

#1545 (Mar 24, 2018, 11:38:37 PM)

1. clarified signature; — wenzelm / hgweb

#1544 (Mar 24, 2018, 10:42:02 PM)

1. clarified messages (amending 3e072441c96a); — wenzelm / hgweb

#1543 (Mar 24, 2018, 9:46:07 PM)

1. session tmp_dir is default master_dir; — wenzelm / hgweb
2. tuned output; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. clarified theory node name;
   purge_theories: return purged, retained;
   tuned documentation; — wenzelm / hgweb

#1542 (Mar 24, 2018, 5:10:11 PM)

1. added lemma — nipkow / hgweb

#1541 (Mar 23, 2018, 11:40:06 PM)

1. added command "purge_theories";
   proper documentation: command "use_theories" is asynchronous; — wenzelm / hgweb
2. clarified signature -- eliminated somewhat pointless positions; — wenzelm / hgweb
3. clarified signature -- more like use_theories; — wenzelm / hgweb
4. clarified; — wenzelm / hgweb
5. removed somewhat pointless argument; — wenzelm / hgweb
6. support for purge_theories; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb

#1540 (Mar 23, 2018, 5:40:08 PM)

1. more robust timing info: do not rely on order of markup; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. field "kind" is always present, with default "writeln"; — wenzelm / hgweb

#1539 (Mar 23, 2018, 11:53:42 AM)

1. merged — nipkow / hgweb
2. eliminated "elems" — nipkow / hgweb

#1538 (Mar 23, 2018, 10:58:07 AM)

1. NEWS and CONTRIBUTORS — haftmann / hgweb

#1537 (Mar 22, 2018, 5:28:10 PM)

1. tuned; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. provide tmp_dir for server session; — wenzelm / hgweb
4. clarified signature: flexible base_dir; — wenzelm / hgweb
5. clarified exported messages, e.g. suppress "information", "tracing";
   export "legacy_feature" as "warning", in accordance to console default output; — wenzelm / hgweb
6. clarified signature: prefer selective include_sessions; — wenzelm / hgweb
7. clarified signature: more uniform session_id; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. clarified signature: do not expose somewhat accidental internal options; — wenzelm / hgweb
10. misc tuning and clarification; — wenzelm / hgweb
11. more documentation; — wenzelm / hgweb
12. clarified result; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. clarified error result, without JSON object from "session_build";
    clarified regular result; — wenzelm / hgweb
15. proper order of matches: Server.Error is an instance of Exn.ERROR; — wenzelm / hgweb
16. clarified result; — wenzelm / hgweb
17. clarified markup according to common Command.Results; — wenzelm / hgweb

#1536 (Mar 22, 2018, 2:01:10 PM)

1. make baliL and baliR symmetric — nipkow / hgweb

#1535 (Mar 22, 2018, 8:19:09 AM)

1. proof of concept for algebraically founded bit lists — haftmann / hgweb
2. tuned proof — haftmann / hgweb
3. prefer convention to place operation name before type name — haftmann / hgweb

#1534 (Mar 20, 2018, 2:43:05 PM)

1. more lemmas — haftmann / hgweb
2. generalized — haftmann / hgweb

#1533 (Mar 19, 2018, 7:34:08 PM)

1. documentation for the Isabelle server; — wenzelm / hgweb
2. clarified message name: disallow single quote; — wenzelm / hgweb

#1532 (Mar 18, 2018, 2:43:08 PM)

1. clarified server shutdown: stop all sessions; — wenzelm / hgweb
2. more explicit error messages;
   clarified signature; — wenzelm / hgweb
3. more explicit errors;
   tuned; — wenzelm / hgweb

#1531 (Mar 18, 2018, 1:13:09 AM)

1. additional Eisbach combinators and utility methods
   
   (by Daniel Matichuck) — kleing / hgweb

#1530 (Mar 17, 2018, 10:15:14 PM)

1. fewer messages; — wenzelm / hgweb

#1529 (Mar 17, 2018, 9:19:06 PM)

1. output result messages; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. more position information; — wenzelm / hgweb
4. more robust check_state loop, even without session activity (e.g. idempotent use_theories); — wenzelm / hgweb
5. synchronized Session.update; — wenzelm / hgweb
6. more interruptible use_theories;
   tuned comments; — wenzelm / hgweb
7. clarified exception handling: include interrupts; — wenzelm / hgweb
8. support for repeated events; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. more interruptible;
    tuned signature; — wenzelm / hgweb
11. unload_theories: actually observe required state;
    misc tuning and clarification; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb

#1528 (Mar 16, 2018, 11:01:09 PM)

1. prefer typed UUID; — wenzelm / hgweb
2. unload_theories after consolidation -- reset node_required;
   proper node_perspective (amending 0d8e4e777973); — wenzelm / hgweb

#1527 (Mar 16, 2018, 7:04:06 PM)

1. support for "use_theories"; — wenzelm / hgweb
2. JSON representation for Position.T; — wenzelm / hgweb
3. interruptible exploration of dependencies; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. tuned message; — wenzelm / hgweb

#1526 (Mar 16, 2018, 2:22:07 PM)

1. proper options; — wenzelm / hgweb
2. tuned options; — wenzelm / hgweb

#1525 (Mar 15, 2018, 11:35:55 PM)

1. more comments; — wenzelm / hgweb
2. tuned message -- more readable JSON; — wenzelm / hgweb

#1524 (Mar 15, 2018, 10:40:05 PM)

1. more accurate isabelle_id: parent directory is not necessarily at tip; — wenzelm / hgweb
2. store session: per Server/Context, not Connection;
   support for "session_stop"; — wenzelm / hgweb
3. clarified server log;
   tuned options; — wenzelm / hgweb
4. support for "session_start"; — wenzelm / hgweb

#1523 (Mar 15, 2018, 5:01:05 PM)

1. updated user name; — wenzelm / hgweb
2. clarified message; — wenzelm / hgweb
3. clarified message; — wenzelm / hgweb
4. more uniform id; — wenzelm / hgweb
5. prefer non-strict defaults; — wenzelm / hgweb
6. clarified default; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb

#1522 (Mar 14, 2018, 8:40:10 PM)

1. asynchronous "session_build"; — wenzelm / hgweb
2. support for asynchronous tasks, with "cancel" command; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. more informative JSON results; — wenzelm / hgweb
5. more informative error with JSON result;
   tuned signature; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb

#1521 (Mar 14, 2018, 4:46:09 PM)

1. misc tuning and clarification; — wenzelm / hgweb

#1520 (Mar 13, 2018, 10:33:14 PM)

1. publish current log file, e.g. for easy error detection; — wenzelm / hgweb

#1519 (Mar 13, 2018, 9:37:09 PM)

1. more options; — wenzelm / hgweb
2. allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose"); — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb

#1518 (Mar 13, 2018, 8:04:09 PM)

1. merged — wenzelm / hgweb
2. added server command "session_build": similar to JEdit_Resources.session_build; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. more flexible preferences: avoid hardwired file;
   tuned signature; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more operations for typed JSON values; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. tuned signature;
    tuned output; — wenzelm / hgweb
11. explicit Server.Context with output channels (concurrent write);
    support for Logger and Progress; — wenzelm / hgweb
12. allow "." in message name; — wenzelm / hgweb
13. re-use existing in/out streams; — wenzelm / hgweb
14. tuned signature -- more generic; — wenzelm / hgweb
15. tuned imports; — wenzelm / hgweb
16. tuned; — wenzelm / hgweb
17. tuned signature; — wenzelm / hgweb
18. clarified signature -- do not expose socket; — wenzelm / hgweb

#1517 (Mar 12, 2018, 9:16:10 PM)

1. Removed stray 'sledgehammer' invocation — Manuel Eberl <eberlm@in.tum.de> / hgweb
2. Changes to NEWS regarding 2a6ef5ba4822 — Manuel Eberl <eberlm@in.tum.de> / hgweb
3. Changes to complete distributive lattices due to Viorel Preoteasa — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1516 (Mar 12, 2018, 11:52:04 AM)

1. eliminiated superfluous class semiring_bits — haftmann / hgweb

#1515 (Mar 11, 2018, 10:00:48 PM)

1. tuned; — wenzelm / hgweb

#1514 (Mar 11, 2018, 9:04:07 PM)

1. tuned; — wenzelm / hgweb
2. update XML cache for slightly modified messages; — wenzelm / hgweb
3. more compact markup tree: output messages are already stored in command results (e.g. relevant for  XML data representation); — wenzelm / hgweb

#1513 (Mar 11, 2018, 4:16:06 PM)

1. more options; — wenzelm / hgweb
2. clarified default server name; — wenzelm / hgweb
3. more uniform output: this may be parsed by another program; — wenzelm / hgweb
4. clarified argument formats: explicit Unit, allow XML.Elem as well;
   tuned messages: prefer single quotes for JSON output; — wenzelm / hgweb
5. tuned comments; — wenzelm / hgweb
6. convenience to represent XML.Body as single XML.Elem; — wenzelm / hgweb
7. clarified AFP partitioning; — wenzelm / hgweb

#1512 (Mar 11, 2018, 8:19:08 AM)

1. abstract algebraic bit operations — haftmann / hgweb

#1511 (Mar 10, 2018, 8:46:06 PM)

1. more balanced AFP partitioning; — wenzelm / hgweb

#1510 (Mar 10, 2018, 4:36:41 PM)

1. workaround for occasional deadlock seen in HOL-Proofs with threads=2; — wenzelm / hgweb
2. adapted to 3869b2400e22; — wenzelm / hgweb

#1509 (Mar 10, 2018, 2:31:06 PM)

1. tuned output; — wenzelm / hgweb
2. more options: client without implicit server startup; — wenzelm / hgweb
3. console interaction with line-editor; — wenzelm / hgweb
4. more flexible message formats; — wenzelm / hgweb
5. clarified interrupt handling; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. option for console interaction; — wenzelm / hgweb
8. more uniform Bytes.read_line/read_block operations; — wenzelm / hgweb
9. auto update; — wenzelm / hgweb
10. more comments; — wenzelm / hgweb
11. more general TTY loop; — wenzelm / hgweb
12. added Reply.NOTE for asynchronous notifications; — wenzelm / hgweb
13. more operations; — wenzelm / hgweb
14. more thorough init: purge inactive entries; — wenzelm / hgweb
15. more generous timeout; — wenzelm / hgweb
16. Entry.connection: proview password here;
    more robust checks; — wenzelm / hgweb
17. clarified initial protocol; — wenzelm / hgweb
18. ignore empty lines; — wenzelm / hgweb
19. tuned; — wenzelm / hgweb
20. more robust read_line after shutdown; — wenzelm / hgweb
21. more implicit wire protocol; — wenzelm / hgweb
22. tuned signature; — wenzelm / hgweb
23. clarified server start, notably for invocation within regular Isabelle/Scala process; — wenzelm / hgweb
24. tuned signature; — wenzelm / hgweb
25. tuned signature; — wenzelm / hgweb
26. clarified toString operations; — wenzelm / hgweb
27. clarified socket connection; — wenzelm / hgweb
28. server commands may access Server;
    Server.stop: proper shutdown;
    clarified signature; — wenzelm / hgweb
29. tuned -- avoid regex matching on potentially large string;
    clarified message: command name could be malformed; — wenzelm / hgweb

#1508 (Mar 8, 2018, 2:25:10 PM)

1. more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X; — wenzelm / hgweb

#1507 (Mar 8, 2018, 11:58:04 AM)

1. clarified notion of unknown files: ignore files outside of a Mercurial repository; — wenzelm / hgweb
2. more balanced AFP partitioning; — wenzelm / hgweb

#1506 (Mar 7, 2018, 7:28:02 PM)

1. more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL); — wenzelm / hgweb
2. tuned -- more uniform; — wenzelm / hgweb
3. eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism; — wenzelm / hgweb

#1505 (Mar 7, 2018, 7:37:03 AM)

1. Drop rewrite rule arguments of sublocale and interpretation implementations. — ballarin / hgweb

#1504 (Mar 6, 2018, 6:37:05 PM)

1. more balanced AFP partitioning; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory; — wenzelm / hgweb
4. more robust: normalize potentially symbolic rev; — wenzelm / hgweb
5. proxy setup for lrzcloud1; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. support for permissive connections, for odd situations where host keys are not accepted; — wenzelm / hgweb
8. proper target directory; — wenzelm / hgweb
9. eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation); — wenzelm / hgweb

#1503 (Mar 4, 2018, 8:55:05 PM)

1. document existing Apache2 configuration; — wenzelm / hgweb

#1502 (Mar 4, 2018, 3:19:04 PM)

1. consolidated main cronjob server on virtual machine together with build_log database;
   eliminated special tricks for Gentoo;
   import plain_identify logs, export all logs for backup;
   run build_release, build_history_base in parallel to remote_build_history tasks; — wenzelm / hgweb
2. identify closer to main cronjob -- avoid diverging changeset versions; — wenzelm / hgweb

#1501 (Mar 4, 2018, 12:34:04 PM)

1. Drop rewrites after defines in interpretations. — ballarin / hgweb

#1500 (Mar 3, 2018, 11:01:30 PM)

1. proper remote_mac according to Admin/Release/CHECKLIST; — wenzelm / hgweb

#1499 (Mar 3, 2018, 10:04:05 PM)

1. more Java heap, e.g. relevant for hg.graph on Isabelle repository; — wenzelm / hgweb
2. more robust check -- do not rely on return code; — wenzelm / hgweb
3. more compact ML_Statistics, to make build_status work with less than 2GB heap; — wenzelm / hgweb
4. retain latest ml_stats (amending e76c6cb0d461); — wenzelm / hgweb

#1498 (Mar 3, 2018, 5:46:11 PM)

1. accomodate smaller build machine; — wenzelm / hgweb

#1497 (Mar 3, 2018, 3:40:06 PM)

1. clarified signature; — wenzelm / hgweb
2. clarified self_update: imitate visible directory state on remote side; — wenzelm / hgweb
3. more operations; — wenzelm / hgweb
4. self_update implies push_isabelle_home (see also 4c253e84ae62); — wenzelm / hgweb
5. uniform setup_repository (pull/clone without update);
   tuned signature; — wenzelm / hgweb
6. clarified signature: facilitate interactive experimentation; — wenzelm / hgweb
7. clarified tasks; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb

#1496 (Mar 2, 2018, 10:00:30 PM)

1. proper order; — wenzelm / hgweb
2. clarified README; — wenzelm / hgweb

#1495 (Mar 2, 2018, 7:54:34 PM)

1. merged — wenzelm / hgweb
2. more ssh options; — wenzelm / hgweb
3. support for proxy connection, similar to ProxyCommand in ssh config; — wenzelm / hgweb
4. prefer https; — wenzelm / hgweb
5. avoid hardwired parameters;
   less ambitious defaults: low memory requirements; — wenzelm / hgweb

#1494 (Mar 2, 2018, 4:34:57 PM)

1. Drop illegitimate optimisation from d5a7f2c54655. — ballarin / hgweb

#1493 (Mar 2, 2018, 2:43:07 PM)

1. Fall back to reading rewrite morphism first if activation fails without it. — ballarin / hgweb
2. Proper rewrite morphisms in locale instances. — ballarin / hgweb

#1492 (Mar 1, 2018, 9:28:05 PM)

1. clarified date for presentation vs. formal pull_date; — wenzelm / hgweb
2. reveal raw data in CSV format; — wenzelm / hgweb
3. support for CSV files; — wenzelm / hgweb
4. tuned comment; — wenzelm / hgweb
5. clarified syntax: reject formal comments explicitly, instead of ignoring them silently; — wenzelm / hgweb

#1491 (Feb 28, 2018, 6:49:15 PM)

1. merged — immler / hgweb
2. generalized lemmas about orthogonal transformation — immler / hgweb

#1490 (Feb 28, 2018, 4:46:04 PM)

1. more explicit infixl (see initial 1edf0f223c6e);
   clarified name; — wenzelm / hgweb
2. clarified use of vec type syntax; — wenzelm / hgweb

#1489 (Feb 26, 2018, 7:31:06 PM)

1. new lemma — haftmann / hgweb
2. dedicated append function for string literals — haftmann / hgweb

#1488 (Feb 26, 2018, 11:22:05 AM)

1. generalized — immler / hgweb
2. moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements — immler / hgweb

#1487 (Feb 25, 2018, 8:31:06 PM)

1. merged — wenzelm / hgweb
2. prefer symbols; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. more abbrevs; — wenzelm / hgweb
5. allow multiple entries of and_list (on both sides); — wenzelm / hgweb
6. eliminated ASCII syntax from Pure bootstrap;
   tuned comments; — wenzelm / hgweb

#1486 (Feb 25, 2018, 5:01:05 PM)

1. merged — paulson / hgweb
2. new material on matrices, etc., and consolidating duplicate results about of_nat — paulson <lp15@cam.ac.uk> / hgweb

#1485 (Feb 25, 2018, 1:46:04 PM)

1. notation for dummy sort; — wenzelm / hgweb

#1484 (Feb 24, 2018, 11:37:06 PM)

1. more symbols; — wenzelm / hgweb

#1483 (Feb 23, 2018, 10:39:12 PM)

1. merged — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. removed unused clone of (map o apsnd);
   removed unused variant of HOLogic.mk_obj_eq; — wenzelm / hgweb
6. prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS; — wenzelm / hgweb
7. added HOLogic.mk_obj_eq convenience and eliminated some clones; — wenzelm / hgweb
8. tuned -- use existing Morphism.instantiate_morphism; — wenzelm / hgweb

#1482 (Feb 23, 2018, 7:17:26 PM)

1. Merged; — Wenda Li <wl302@cam.ac.uk> / hgweb
2. merged — Wenda Li <wl302@cam.ac.uk> / hgweb
3. Unified the order of zeros and poles; improved reasoning around non-essential singularites — Wenda Li <wl302@cam.ac.uk> / hgweb

#1481 (Feb 23, 2018, 4:55:06 PM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. tuned signature -- eliminated clones; — wenzelm / hgweb
4. command 'interpret' no longer exposes resulting theorems as literal facts; — wenzelm / hgweb
5. more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate; — wenzelm / hgweb
8. explicit operations to instantiate frees: typ, term, thm, morphism; — wenzelm / hgweb
9. more operations for ctyp, cterm; — wenzelm / hgweb
10. minor tuning and clarification; — wenzelm / hgweb
11. minor tuning and clarification; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb

#1480 (Feb 23, 2018, 1:37:06 PM)

1. fixed the proof of pair_measure_count_space — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring — paulson <lp15@cam.ac.uk> / hgweb
4. merged — paulson / hgweb
5. type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0 — paulson <lp15@cam.ac.uk> / hgweb

#1479 (Feb 23, 2018, 8:10:04 AM)

1. simplified Radix_Sort — nipkow / hgweb

#1478 (Feb 22, 2018, 9:46:21 PM)

1. merged — immler / hgweb
2. merged — immler / hgweb
3. moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations — immler / hgweb

#1477 (Feb 22, 2018, 7:55:06 PM)

1. simplified def of stable — nipkow / hgweb

#1476 (Feb 21, 2018, 3:10:07 PM)

1. Lots of new material about matrices, etc. — paulson <lp15@cam.ac.uk> / hgweb

#1475 (Feb 20, 2018, 10:49:08 PM)

1. tuned proofs -- prefer explicit names for facts from 'interpret'; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e); — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. use lazy notes for locale context init and later additions of facts; — wenzelm / hgweb
7. avoid premature Lazy.force due to strict "?" operator; — wenzelm / hgweb

#1474 (Feb 20, 2018, 10:55:03 AM)

1. Merge — paulson <lp15@cam.ac.uk> / hgweb
2. Merge — paulson <lp15@cam.ac.uk> / hgweb
3. lots of new material, ultimately related to measure theory — paulson <lp15@cam.ac.uk> / hgweb

#1473 (Feb 19, 2018, 10:49:07 PM)

1. merged — wenzelm / hgweb
2. support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
   register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel);
   support for lazy notes for locale activation (still inactive); — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. tuned: more parallel; — wenzelm / hgweb
5. clarified modules; — wenzelm / hgweb
6. clarified modules; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb
10. tuned: more accurate transfer; — wenzelm / hgweb
11. store facts as lazy values; — wenzelm / hgweb
12. clarified operations; — wenzelm / hgweb
13. misc tuning and clarification; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. clarified modules; — wenzelm / hgweb
16. more operations; — wenzelm / hgweb

#1472 (Feb 19, 2018, 4:07:02 PM)

1. added lemma — nipkow / hgweb

#1471 (Feb 18, 2018, 9:07:07 PM)

1. tuned; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. misc tuning and clarification;
   removed unused all_registrations_of; — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. more explicit instantiate_morphism (without checks for typ / term component); — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. tuned signature; — wenzelm / hgweb

#1470 (Feb 17, 2018, 8:16:06 PM)

1. more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings(); — wenzelm / hgweb
2. avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>"; — wenzelm / hgweb
3. trim context of persistent data; — wenzelm / hgweb
4. trim context of persistent data; — wenzelm / hgweb
5. trim context of persistent data; — wenzelm / hgweb
6. clarified apply_transaction: always continue without presentation context; — wenzelm / hgweb
7. more tight presentation context: avoid storing full Toplevel.state; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. more informative theories_trace; — wenzelm / hgweb

#1469 (Feb 17, 2018, 12:01:06 PM)

1. merged — wenzelm / hgweb
2. tuned signature (again); — wenzelm / hgweb
3. trim context of persistent data; — wenzelm / hgweb
4. trim context of persistent data; — wenzelm / hgweb
5. proper file name; — wenzelm / hgweb
6. trim context of persistent data;
   tuned signature; — wenzelm / hgweb
7. clarified data operations, with trim_context and transfer; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. trim context of persistent data;
   tuned; — wenzelm / hgweb
10. trim context of persistent data; — wenzelm / hgweb
11. removed unused material; — wenzelm / hgweb
12. trim context of persistent data; — wenzelm / hgweb
13. trim context of persistent data;
    no need to trim context for del operations; — wenzelm / hgweb
14. tuned; — wenzelm / hgweb
15. tuned whitespace; — wenzelm / hgweb
16. more operations; — wenzelm / hgweb
17. optional trace of created theory values; — wenzelm / hgweb
18. more operations; — wenzelm / hgweb
19. auxiliary operation for space profiling; — wenzelm / hgweb

#1468 (Feb 16, 2018, 7:07:06 PM)

1. special treatment of 0 only refers to type char — haftmann / hgweb

#1467 (Feb 16, 2018, 4:28:50 PM)

1. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
2. features and caveats of datatype_record — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1466 (Feb 16, 2018, 1:07:04 PM)

1. merged — Andreas Lochbihler / hgweb
2. strengthen filter relator to canonical categorical definition with better properties — Andreas Lochbihler / hgweb

#1465 (Feb 15, 2018, 3:52:05 PM)

1. recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks; — wenzelm / hgweb

#1464 (Feb 15, 2018, 1:28:04 PM)

1. merged — wenzelm / hgweb
2. more symbols; — wenzelm / hgweb

#1463 (Feb 14, 2018, 4:40:04 PM)

1. New theory ex/Radix_Sort.thy — nipkow / hgweb

#1462 (Feb 14, 2018, 1:25:03 PM)

1. records based on datatypes/BNF infrastructure — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1461 (Feb 13, 2018, 3:04:03 PM)

1. updated polyml component; — wenzelm / hgweb
2. no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples); — wenzelm / hgweb

#1460 (Feb 13, 2018, 12:19:07 PM)

1. retain remote_builds_old for build_status; — wenzelm / hgweb
2. lxbroy7 no longer exists; — wenzelm / hgweb

#1459 (Feb 12, 2018, 8:25:03 PM)

1. added lemmas — nipkow / hgweb

#1458 (Feb 12, 2018, 2:57:24 PM)

1. corrected some URLs — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1457 (Feb 12, 2018, 2:01:04 PM)

1. permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc; — wenzelm / hgweb

#1456 (Feb 12, 2018, 8:58:08 AM)

1. merged — wenzelm / hgweb
2. updated polyml component -- omitting bad polyml-5.7.1-3; — wenzelm / hgweb
3. use preferred resolver according to DOI Handbook §3.8 — Lars Hupel <lars.hupel@mytum.de> / hgweb
4. no --enable-shared for x86_64-darwin: does not work on some test machine; — wenzelm / hgweb
5. proper target directory; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more robust options; — wenzelm / hgweb
8. back to --disable-shared on windows to avoid odd core-dump of polyimport; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. back to --disable-shared on x86-darwin to avoid odd core-dump of polyimport; — wenzelm / hgweb
11. clarified command-line defaults; — wenzelm / hgweb
12. enforce shared libpoly on all platforms, with File.copy before File.move; — wenzelm / hgweb

#1455 (Feb 10, 2018, 1:22:05 PM)

1. NEWS; — wenzelm / hgweb
2. updated to polyml-5.7.1-2, which includes libgmp for x86-darwin as well; — wenzelm / hgweb
3. support for libgmp for x86-darwin; — wenzelm / hgweb
4. more accessible src/Pure/ROOT.ML; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb

#1454 (Feb 9, 2018, 9:04:05 PM)

1. more robust: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses); — wenzelm / hgweb
2. rebuild of polyml-5.7.1 with libgmp for x86_darwin; — wenzelm / hgweb
3. patch polyc: avoid hardwired directory prefix; — wenzelm / hgweb
4. support for libgmp for x86_64-darwin; — wenzelm / hgweb
5. built-in library path for (optional) libgmp on macos; — wenzelm / hgweb
6. removed obsolete polyi executable: change of DYLD_LIBRARY_PATH is not required; — wenzelm / hgweb
7. more robust access to shared libraries for poly executable: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses); — wenzelm / hgweb

#1453 (Feb 8, 2018, 4:09:18 PM)

1. Merged — eberlm <eberlm@in.tum.de> / hgweb
2. Some lemmas about complex sinh/cosh/tanh — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1452 (Feb 8, 2018, 1:43:04 PM)

1. more elementary proof of connected_Times, earlier — immler / hgweb

#1451 (Feb 8, 2018, 9:07:06 AM)

1. merged — nipkow / hgweb
2. tuned — nipkow / hgweb

#1450 (Feb 7, 2018, 9:07:04 PM)

1. Added hyperbolic functions — eberlm <eberlm@in.tum.de> / hgweb

#1449 (Feb 5, 2018, 9:43:06 AM)

1. added lemmas, avoid 'float_of 0' — immler / hgweb

#1448 (Feb 3, 2018, 9:34:07 PM)

1. clarified signature; — wenzelm / hgweb
2. more uniform treatment of formal comments within document source;
   more robust nesting; — wenzelm / hgweb
3. just one check of formal comments; — wenzelm / hgweb
4. avoid proliferation of language_document reports;
   clarified signature; — wenzelm / hgweb
5. more external tools for AFP test; — wenzelm / hgweb
6. clarified overall range: include delimiters; — wenzelm / hgweb

#1447 (Feb 2, 2018, 11:55:03 AM)

1. added lemma — nipkow / hgweb

#1446 (Feb 1, 2018, 9:19:04 PM)

1. tuned: more standard use of order; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. clarified signature;
   eliminated aliases of Thm.term_ord; — wenzelm / hgweb
5. clarified signature: prefer proper order operation; — wenzelm / hgweb
6. tuned signature: more operations; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb

#1445 (Jan 31, 2018, 9:40:02 PM)

1. proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)"; — wenzelm / hgweb

#1444 (Jan 31, 2018, 3:58:06 PM)

1. performance fine-tuning of hot spot; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more efficient tokens_match_ord based on token_kind_index;
   tuned; — wenzelm / hgweb
4. more abstract type; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. explicit dummy token; — wenzelm / hgweb
9. clarified modules; — wenzelm / hgweb
10. clarified signature; — wenzelm / hgweb

#1443 (Jan 31, 2018, 12:36:32 AM)

1. clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area; — wenzelm / hgweb
2. clarified lines: like split_lines; — wenzelm / hgweb

#1442 (Jan 30, 2018, 10:46:04 PM)

1. tuned; — wenzelm / hgweb
2. unused; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. simplified: prod_count is always NONE; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. tuned data structure and operations; — wenzelm / hgweb
7. tuned data structure and operations; — wenzelm / hgweb
8. tuned data structure and operations; — wenzelm / hgweb
9. more operations; — wenzelm / hgweb
10. prefer specific tokens_subtract: subtle change of comparison via tokens_match; — wenzelm / hgweb
11. tuned type: absorb NONE: token option as token_none: token; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. clarified types and operations: potentially more efficient add_prods;
    tuned data structure; — wenzelm / hgweb
14. clarified modules;
    tuned; — wenzelm / hgweb
15. tuned: more explicit types; — wenzelm / hgweb

#1441 (Jan 30, 2018, 12:24:50 AM)

1. tuned data structure: potentially more efficient add_prods; — wenzelm / hgweb
2. clarified operations; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these; — wenzelm / hgweb

#1440 (Jan 29, 2018, 8:58:03 PM)

1. irrelevant reference to doubtful theory Code_Char — haftmann / hgweb
2. avoid concrete (anti)mono in theorem names since it could be the other way round — haftmann / hgweb

#1439 (Jan 29, 2018, 7:34:03 PM)

1. more uniform documentation; — wenzelm / hgweb

#1438 (Jan 29, 2018, 11:31:06 AM)

1. proper fall-back rendering of control symbol; — wenzelm / hgweb

#1437 (Jan 28, 2018, 9:01:08 PM)

1. clarified take/drop/chop prefix/suffix; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb

#1436 (Jan 28, 2018, 1:07:07 PM)

1. proper signature (amending c4e9e0c50487); — wenzelm / hgweb

#1435 (Jan 27, 2018, 9:16:07 PM)

1. tuned output; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. explicit graph for chains, which contains all nts as nodes; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. prefer lazy update; — wenzelm / hgweb
7. tuned output; — wenzelm / hgweb
8. more operations; — wenzelm / hgweb

#1434 (Jan 27, 2018, 10:37:02 AM)

1. include lemmas generally useful for combinatorial proofs — bulwahn / hgweb

#1433 (Jan 26, 2018, 9:22:04 PM)

1. redundant; — wenzelm / hgweb

#1432 (Jan 26, 2018, 11:58:06 AM)

1. allow cartouche within ML string; — wenzelm / hgweb
2. verbatim output consists of plain lines; — wenzelm / hgweb
3. old-style inner comments are legacy; — wenzelm / hgweb
4. more markup: disable spell-checker for raw latex; — wenzelm / hgweb
5. clarified signature: items with \isasep are special; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. tuned message; — wenzelm / hgweb
8. clarified operations; — wenzelm / hgweb
9. tuned signature: removed unused operations; — wenzelm / hgweb
10. tuned: prefer list operations over Source.source;
    approximative parsing of theory header; — wenzelm / hgweb
11. tuned: prefer list operations over Source.source; — wenzelm / hgweb
12. tuned: prefer list operations over Source.source; — wenzelm / hgweb
13. clarified signature; — wenzelm / hgweb
14. clarified position; — wenzelm / hgweb
15. clarified operations; — wenzelm / hgweb

#1431 (Jan 23, 2018, 9:22:07 PM)

1. merged — wenzelm / hgweb
2. treat sessions as entities with defining position;
   tuned signature; — wenzelm / hgweb
3. options file for x86_64 only (amending 03a96b8c7c06); — wenzelm / hgweb
4. updated to jdk-8u162; — wenzelm / hgweb
5. more robust java.ext.dirs: avoid picking up accidental jars from system directories; — wenzelm / hgweb

#1430 (Jan 23, 2018, 6:22:05 PM)

1. drop redundant cong rules — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1429 (Jan 22, 2018, 10:52:02 PM)

1. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
2. drop redundant fundef_cong rule — Lars Hupel <lars.hupel@mytum.de> / hgweb
3. tuned — Lars Hupel <lars.hupel@mytum.de> / hgweb
4. repair malformed fundef_cong rule — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1428 (Jan 22, 2018, 3:31:05 PM)

1. removed duplicate — nipkow / hgweb

#1427 (Jan 22, 2018, 11:40:05 AM)

1. tuned message: same error may occur in different contexts; — wenzelm / hgweb

#1426 (Jan 21, 2018, 3:04:22 PM)

1. detect more errors; — wenzelm / hgweb

#1425 (Jan 21, 2018, 11:10:07 AM)

1. merged — nipkow / hgweb
2. made sorted fun again — nipkow / hgweb
3. imported patch sorted — nipkow / hgweb

#1424 (Jan 20, 2018, 3:58:05 PM)

1. add lemma on lists from Falling_Factorial_Sum entry — bulwahn / hgweb

#1423 (Jan 19, 2018, 10:42:00 PM)

1. merged — wenzelm / hgweb
2. avoid evaluation of embedded comment; — wenzelm / hgweb
3. disable "display" style in marginal (line) comment; — wenzelm / hgweb
4. more uniform output of source / text / theory_text, with handling of formal comments etc.; — wenzelm / hgweb
5. sort completion result; — wenzelm / hgweb
6. recovered antiquotation check without latex mode (cf. dfc93f2b01ea); — wenzelm / hgweb
7. formal treatment of documentation names; — wenzelm / hgweb
8. support for completion; — wenzelm / hgweb
9. adapted to a5ca98950a91; — wenzelm / hgweb
10. tuned output of plain name; — wenzelm / hgweb
11. clarified signature; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. unused; — wenzelm / hgweb
15. clarified access to antiquotation options;
    define explicit variants of antiquotations;
    output proper Latex.text;
    misc tuning and clarification; — wenzelm / hgweb
16. more operations; — wenzelm / hgweb
17. tuned signature; — wenzelm / hgweb
18. discontinued unused wrapper: print_mode is provided directly; — wenzelm / hgweb

#1422 (Jan 19, 2018, 5:19:12 PM)

1. corrected name — nipkow / hgweb
2. moved from AFP/Gromov — nipkow / hgweb

#1421 (Jan 19, 2018, 12:25:05 PM)

1. moved from AFP/Gromov — nipkow / hgweb

#1420 (Jan 19, 2018, 8:34:04 AM)

1. added lemma — nipkow / hgweb

#1419 (Jan 18, 2018, 6:22:02 PM)

1. moved from AFP/Gromov — nipkow / hgweb
2. moved t3/t4 space from AFP/Gromov to here. — nipkow / hgweb

#1418 (Jan 18, 2018, 10:04:04 AM)

1. more automation — nipkow / hgweb

#1417 (Jan 17, 2018, 2:37:05 PM)

1. more lemmas by Gouezele — nipkow / hgweb
2. move lemmas by Gouezel to distribution — nipkow / hgweb

#1416 (Jan 16, 2018, 7:34:06 PM)

1. Experimental support for rewrite morphisms in locale instances. — ballarin / hgweb

#1415 (Jan 16, 2018, 5:38:56 PM)

1. tuned signature; — wenzelm / hgweb

#1414 (Jan 16, 2018, 3:49:06 PM)

1. more documentation; — wenzelm / hgweb
2. clarified markup; — wenzelm / hgweb
3. discontinued old form of marginal comments; — wenzelm / hgweb

#1413 (Jan 16, 2018, 10:19:08 AM)

1. tuned document; — wenzelm / hgweb
2. clarified comments; — wenzelm / hgweb
3. standardized towards new-style formal comments: isabelle update_comments; — wenzelm / hgweb
4. uniform treatment of old-style and new-style comments; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. clarified markup; — wenzelm / hgweb
7. more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>; — wenzelm / hgweb
8. clarified modules;
   more operations; — wenzelm / hgweb

#1412 (Jan 15, 2018, 10:52:04 AM)

1. tuned — nipkow / hgweb

#1411 (Jan 14, 2018, 10:22:08 PM)

1. eliminated clones; — wenzelm / hgweb
2. trim blanks -- more thoroughly than in update_cartouches (for single-line comments); — wenzelm / hgweb
3. more operations (as in ML); — wenzelm / hgweb
4. more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages; — wenzelm / hgweb
5. clarified Token.is_text (cf. Parse.text in ML); — wenzelm / hgweb
6. more operations; — wenzelm / hgweb
7. support for completion; — wenzelm / hgweb
8. allow LaTeX source as formal comment; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. clarified SML (no formal comments) vs. Isabelle/ML (arbitrary comments); — wenzelm / hgweb
11. clarified signature; — wenzelm / hgweb
12. clarified modules: uniform notion of formal comments; — wenzelm / hgweb

#1410 (Jan 13, 2018, 11:06:38 PM)

1. added glyph from "Deja Vu Sans Mono" font; — wenzelm / hgweb

#1409 (Jan 13, 2018, 9:16:07 PM)

1. tuned messages; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1); — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. more general error suffixes, e.g. for messages that are broken over several lines; — wenzelm / hgweb
7. another Latex error seen in the wild:
   Undefined control sequence.
   \isamarkupcancel #1->\xout — wenzelm / hgweb
8. clarified default; — wenzelm / hgweb
9. clarified formal comments; — wenzelm / hgweb
10. prefer formal comments; — wenzelm / hgweb
11. added \<^cancel> operator for unused text; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb

#1408 (Jan 13, 2018, 3:34:06 PM)

1. restored naming of lemmas after corresponding constants — haftmann / hgweb

#1407 (Jan 12, 2018, 6:55:29 PM)

1. prefer formal comments; — wenzelm / hgweb

#1406 (Jan 12, 2018, 5:22:04 PM)

1. prefer formal text; — wenzelm / hgweb
2. prefer formal comments; — wenzelm / hgweb
3. prefer formal comments; — wenzelm / hgweb

#1405 (Jan 12, 2018, 2:16:04 PM)

1. isabelle update_cartouches -c; — wenzelm / hgweb

#1404 (Jan 11, 2018, 1:55:07 PM)

1. uniform use of Standard ML op-infix -- eliminated warnings; — wenzelm / hgweb
2. proper infix; — wenzelm / hgweb

#1403 (Jan 11, 2018, 10:19:05 AM)

1. line break before op was intentional — nipkow / hgweb

#1402 (Jan 10, 2018, 10:20:23 PM)

1. typo — nipkow / hgweb

#1401 (Jan 10, 2018, 7:01:17 PM)

1. tuned notation — nipkow / hgweb
2. tuned — nipkow / hgweb

#1400 (Jan 10, 2018, 3:40:06 PM)

1. ran isabelle update_op on all sources — nipkow / hgweb
2. Manual updates towards conversion of "op" syntax — nipkow / hgweb

#1399 (Jan 10, 2018, 1:56:01 PM)

1. tuned op — nipkow / hgweb

#1398 (Jan 10, 2018, 12:43:05 PM)

1. tuned op's — nipkow / hgweb

#1397 (Jan 9, 2018, 9:52:07 PM)

1. more accurate spell-checking for nested quotations / antiquotations, notably in formal comments; — wenzelm / hgweb
2. uniform typesetting of \isamarkupcmt and \isasymcomment; — wenzelm / hgweb
3. more accurate position for enclosing cartouche; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. clarified presentation_state with provide presentation_context; — wenzelm / hgweb
7. show only symbols with code; — wenzelm / hgweb
8. clarified markup: more like outer syntax side-comment; — wenzelm / hgweb
9. clarified rail token language: white space and formal comments; — wenzelm / hgweb
10. clarified modules; — wenzelm / hgweb
11. removed duplicate text; — wenzelm / hgweb
12. clarified exception; — wenzelm / hgweb

#1396 (Jan 9, 2018, 12:28:07 AM)

1. merged; — wenzelm / hgweb
2. updated to 146757999c8d; — wenzelm / hgweb
3. theory Pure is default presentation context; — wenzelm / hgweb
4. clarified implicit Pure.thy; — wenzelm / hgweb
5. prefer qualified names; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. check formal comments recursively, within arbitrary cartouches (unknown sublanguages); — wenzelm / hgweb
8. more operations; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. clarified output (see also 909dcdec2122, 34d1913f0b20); — wenzelm / hgweb
11. more operations; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb

#1395 (Jan 8, 2018, 6:16:05 PM)

1. moved in some material from Euler-MacLaurin — paulson <lp15@cam.ac.uk> / hgweb

#1394 (Jan 7, 2018, 10:52:06 PM)

1. merged — wenzelm / hgweb
2. prefer formal comments; — wenzelm / hgweb
3. clarified NEWS; — wenzelm / hgweb
4. tuned whitespace; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. support for formal comments in ML in Isabelle/Scala; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. tuned message; — wenzelm / hgweb
9. allow formal comments in ML;
   ML_Compiler.eval: always suppress comments; — wenzelm / hgweb
10. clarified modules; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more uniform output: formal comments within {* ... *}; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. clarified output: avoid extra space; — wenzelm / hgweb
15. output token content with formal comments and antiquotations; — wenzelm / hgweb
16. tuned; — wenzelm / hgweb
17. clarified signature; — wenzelm / hgweb
18. clarified modules; — wenzelm / hgweb
19. inner syntax comments may be written as "\<comment> \<open>text\<close>"; — wenzelm / hgweb

#1393 (Jan 7, 2018, 11:19:06 AM)

1. spelling — haftmann / hgweb

#1392 (Jan 6, 2018, 11:01:03 PM)

1. corrected op — nipkow / hgweb

#1391 (Jan 6, 2018, 5:46:07 PM)

1. tuned op — nipkow / hgweb
2. tuned op — nipkow / hgweb
3. tuned op — nipkow / hgweb

#1390 (Jan 6, 2018, 3:13:06 PM)

1. tuned op — nipkow / hgweb

#1389 (Jan 6, 2018, 1:10:06 PM)

1. tuned op's — nipkow / hgweb

#1388 (Jan 6, 2018, 10:43:20 AM)

1. tuned op — nipkow / hgweb

#1387 (Jan 6, 2018, 9:46:06 AM)

1. tuned op — nipkow / hgweb

#1386 (Jan 5, 2018, 8:26:09 PM)

1. tuned op's — nipkow / hgweb

#1385 (Jan 5, 2018, 6:46:04 PM)

1. Renamed (^) to [^] in preparation of the move from "op X" to (X) — nipkow / hgweb

#1384 (Jan 5, 2018, 3:31:06 PM)

1. tuned op — nipkow / hgweb

#1383 (Jan 4, 2018, 6:25:08 PM)

1. HOL-Analysis: add set_integrable_restrict_space — hoelzl / hgweb

#1382 (Jan 4, 2018, 9:25:05 AM)

1. more correct parentheses — haftmann / hgweb

#1381 (Jan 3, 2018, 10:55:07 PM)

1. more tight HTML output: avoid extra lines within <pre>; — wenzelm / hgweb
2. HTML output for Markdown elements;
   clarified HTML operations; — wenzelm / hgweb

#1380 (Jan 3, 2018, 12:55:08 PM)

1. updated NEWS — blanchet / hgweb
2. removed dead code — blanchet / hgweb
3. removed old 'add_datatype' ML functions — blanchet / hgweb
4. kill old size infrastructure — blanchet / hgweb

#1379 (Jan 3, 2018, 2:32:34 AM)

1. repaired whitespace accident from 2505cabfc515 — haftmann / hgweb
2. proper namespace for evaluators — haftmann / hgweb
3. tuned — haftmann / hgweb
4. more correct name resolving — haftmann / hgweb
5. skip abstract constructors silently in datatype clauses of computations — haftmann / hgweb
6. removed para about 'old_datatype' in docs — blanchet / hgweb

#1378 (Jan 2, 2018, 9:28:18 PM)

1. old_datatype no longer exists (cf. 706b1cf7b76d); — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. PIDE markup for Markdown items (which may consist of multiple paragraphs or lists); — wenzelm / hgweb
4. clarified terminology of "markdown_bullet"; — wenzelm / hgweb
5. compile — blanchet / hgweb
6. updated dependencies + compile — blanchet / hgweb
7. moved 'realizers' into their own theory, now that they are decupled from the old datatype construction — blanchet / hgweb
8. removed 'old_datatype' command — blanchet / hgweb
9. don't test 'old_datatype', which is on its way out — blanchet / hgweb
10. ported inductive realizer to new datatype package — blanchet / hgweb
11. removed needless theorems — blanchet / hgweb

#1377 (Jan 2, 2018, 3:08:37 PM)

1. store high-level 'size' equations — blanchet / hgweb

#1376 (Jan 2, 2018, 1:22:04 PM)

1. avoid call to function that may throw an exception in error message — blanchet / hgweb

#1375 (Jan 2, 2018, 12:25:08 AM)

1. misc tuning and modernization; — wenzelm / hgweb
2. more completion templates; — wenzelm / hgweb
3. proper purge of auxiliary bibtex theory; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb

#1374 (Dec 31, 2017, 10:49:05 PM)

1. Restored correct spacing for set comprehensions — paulson <lp15@cam.ac.uk> / hgweb

#1373 (Dec 30, 2017, 11:31:04 PM)

1. less redundant; — wenzelm / hgweb

#1372 (Dec 30, 2017, 10:01:04 PM)

1. more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html); — wenzelm / hgweb

#1371 (Dec 30, 2017, 8:37:03 PM)

1. more robust treatment of conflicts with existing Unicode text; — wenzelm / hgweb

#1370 (Dec 30, 2017, 2:22:08 PM)

1. tuned whitespace; — wenzelm / hgweb

#1369 (Dec 29, 2017, 11:19:08 PM)

1. no check for bibtex entries from other sessions; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. more accurate message patterns; — wenzelm / hgweb
4. prefer formal citations;
   more accurate bibtex entries; — wenzelm / hgweb
5. proper bibtex entries; — wenzelm / hgweb
6. formal check of @{cite} bibtex entries -- only in batch-mode session builds; — wenzelm / hgweb

#1368 (Dec 28, 2017, 11:52:08 PM)

1. clarified check, notably for bibtex theory (amending 5f082b1fa9fa); — wenzelm / hgweb
2. NEWS; — wenzelm / hgweb
3. proper check for imports, not just ROOT entries; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. implicit thy_load context for bibtex files (VSCode); — wenzelm / hgweb
6. bibtex theory is always required and thus eventually consolidated; — wenzelm / hgweb
7. implicit thy_load context for bibtex files; — wenzelm / hgweb
8. clarified signature: prefer Document.Node.Name.is_bibtex; — wenzelm / hgweb
9. avoid spurious noise: Prover IDE is meant to check for errors; — wenzelm / hgweb
10. clarified signature; — wenzelm / hgweb
11. avoid clash with special files in HTML output; — wenzelm / hgweb
12. unused; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb
14. prefer existing Resources.check_path; — wenzelm / hgweb
15. more accurate bibtex entries; — wenzelm / hgweb
16. added command 'bibtex_file' (for PIDE interaction only); — wenzelm / hgweb
17. clarified default position for empty message pos; — wenzelm / hgweb

#1367 (Dec 25, 2017, 11:31:04 AM)

1. spelling — haftmann / hgweb

#1366 (Dec 24, 2017, 11:10:06 PM)

1. Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume — eberlm <eberlm@in.tum.de> / hgweb

#1365 (Dec 24, 2017, 3:01:05 PM)

1. fewer warnings; — wenzelm / hgweb
2. clarified positions; — wenzelm / hgweb
3. check bibtex database on ML side -- for semantic PIDE editing;
   tuned signature; — wenzelm / hgweb
4. clarified directories; — wenzelm / hgweb

#1364 (Dec 24, 2017, 12:58:08 PM)

1. more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default); — wenzelm / hgweb

#1363 (Dec 23, 2017, 11:19:07 PM)

1. check bibtex database: errors and warnings; — wenzelm / hgweb

#1362 (Dec 23, 2017, 8:49:06 PM)

1. more symbols; — wenzelm / hgweb

#1361 (Dec 23, 2017, 3:13:27 AM)

1. Merge — paulson <lp15@cam.ac.uk> / hgweb
2. Merge — paulson <lp15@cam.ac.uk> / hgweb
3. new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product — paulson <lp15@cam.ac.uk> / hgweb

#1360 (Dec 22, 2017, 11:07:24 PM)

1. more symbols; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb

#1359 (Dec 22, 2017, 9:19:04 PM)

1. store full blob source for the sake of markup_to_XML; — wenzelm / hgweb
2. PIDE markup for non-theory nodes; — wenzelm / hgweb
3. discontinued 'display_drafts' command; — wenzelm / hgweb
4. action "isabelle.draft" for plain-text preview; — wenzelm / hgweb
5. NEWS; — wenzelm / hgweb
6. uniform preview for Isabelle/jEdit and Isabelle/VSCode; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. clarified URL: unique node name; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. proper title;
    clarified modules; — wenzelm / hgweb
11. HTML rendering of \<^control> as in Isabelle/jEdit; — wenzelm / hgweb
12. auto update; — wenzelm / hgweb
13. clarified modules; — wenzelm / hgweb
14. proper HTML title; — wenzelm / hgweb
15. tuned signature; — wenzelm / hgweb

#1358 (Dec 21, 2017, 11:41:21 PM)

1. tuned output; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. isabelle.preview presents bibtex database files as well; — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. isabelle.preview presents auxiliary text files as well; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. tuned signature; — wenzelm / hgweb
8. bibtex HTML output via external tool; — wenzelm / hgweb

#1357 (Dec 21, 2017, 10:19:08 PM)

1. merged — nipkow / hgweb
2. tuned op's — nipkow / hgweb
3. tuned op's — nipkow / hgweb
4. tuned op's — nipkow / hgweb
5. tuned op's — nipkow / hgweb
6. tuned op's — nipkow / hgweb
7. tuned op's — nipkow / hgweb

#1356 (Dec 21, 2017, 1:31:20 PM)

1. tuned; — wenzelm / hgweb

#1355 (Dec 21, 2017, 10:16:05 AM)

1. Some lemmas on complex numbers and coprimality — eberlm <eberlm@in.tum.de> / hgweb

#1354 (Dec 20, 2017, 10:13:05 PM)

1. merged — nipkow / hgweb
2. tuned op's — nipkow / hgweb
3. tuned op's — nipkow / hgweb
4. tuned op's — nipkow / hgweb
5. tuned op's — nipkow / hgweb
6. tuned op's — nipkow / hgweb

#1353 (Dec 20, 2017, 6:58:04 PM)

1. updated URL; — wenzelm / hgweb

#1352 (Dec 20, 2017, 11:52:04 AM)

1. isabelle update_cartouches -c -t; — wenzelm / hgweb

#1351 (Dec 19, 2017, 2:58:03 PM)

1. have 'try0' display results faster — blanchet / hgweb

#1350 (Dec 18, 2017, 8:34:03 PM)

1. a conditional paramitrecity prover — traytel / hgweb

#1349 (Dec 18, 2017, 12:10:03 PM)

1. removed debug output — traytel / hgweb

#1348 (Dec 17, 2017, 8:49:06 AM)

1. made tactics more robust — traytel / hgweb

#1347 (Dec 16, 2017, 11:01:12 PM)

1. tuned; — wenzelm / hgweb
2. more markup;
   multiple error output; — wenzelm / hgweb
3. added document antiquotation @{session name};
   renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation; — wenzelm / hgweb
4. more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0"); — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. disallow theory name "ROOT"; — wenzelm / hgweb
7. PIDE markup for session ROOT files; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. more operations; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. recovered Options.default_markup, e.g. for src/Doc/antiquote_setup.ML (amending 16519cd83ed4); — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. clarified signature; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb

#1346 (Dec 15, 2017, 6:52:07 PM)

1. dedicated case option for code generation to Scala — haftmann / hgweb

#1345 (Dec 14, 2017, 10:13:06 PM)

1. minor performance tuning, notably for Library.fold_string etc.; — wenzelm / hgweb
2. clarified file name; — wenzelm / hgweb
3. purge log files -- avoid old errors; — wenzelm / hgweb
4. expose bibtex errors; — wenzelm / hgweb

#1344 (Dec 14, 2017, 3:07:05 PM)

1. proper exception; — wenzelm / hgweb
2. proper \isakeeptag (amending 13b5c3ff1954); — wenzelm / hgweb
3. tuned; — wenzelm / hgweb

#1343 (Dec 14, 2017, 11:52:04 AM)

1. NEWS; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. purge more carefully (amending 26f548370e8d);
   recovered 'display_drafts'; — wenzelm / hgweb
4. more error information according to @<Print type of token list@> in pdfweb.tex; — wenzelm / hgweb
5. avoid redundant positions; — wenzelm / hgweb
6. positions as postlude: avoid intrusion of odd %-forms into main tex source; — wenzelm / hgweb
7. scan only one line, for more detailed positions; — wenzelm / hgweb
8. purge more thoroughly; — wenzelm / hgweb
9. option document_positions; — wenzelm / hgweb
10. clarified file pattern; — wenzelm / hgweb
11. ensure separation of TeX tokens; — wenzelm / hgweb
12. simplified positions -- line is also human-readable in generated .tex file; — wenzelm / hgweb
13. tuned message; — wenzelm / hgweb
14. avoid excessive whitespace between antiquotations and text; — wenzelm / hgweb
15. updated documentation; — wenzelm / hgweb
16. more robust range on preceding comment-line;
    no range for blank lines;
    avoid recursive output_text/mark_range;
    clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range); — wenzelm / hgweb
17. proper file; — wenzelm / hgweb
18. clarified file positions; — wenzelm / hgweb
19. more operations; — wenzelm / hgweb
20. tuned messages; — wenzelm / hgweb
21. clean log file on Windows; — wenzelm / hgweb
22. avoid println with its extra CR on Windows; — wenzelm / hgweb
23. removed obsolete option (see 74a1b722507e); — wenzelm / hgweb
24. re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here; — wenzelm / hgweb
25. removed Emacs legacy; — wenzelm / hgweb
26. more robust Windows support; — wenzelm / hgweb
27. more explicit latex errors; — wenzelm / hgweb
28. some support for LaTeX; — wenzelm / hgweb

#1342 (Dec 13, 2017, 7:34:06 PM)

1. added lemmas — nipkow / hgweb

#1341 (Dec 13, 2017, 1:35:40 PM)

1. added min_list and arg_min_list — nipkow / hgweb

#1340 (Dec 13, 2017, 11:52:05 AM)

1. made arg_min_on definition — nipkow / hgweb

#1339 (Dec 13, 2017, 9:10:04 AM)

1. added lemmas — nipkow / hgweb

#1338 (Dec 12, 2017, 12:04:05 PM)

1. Moved analysis material from AFP — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1337 (Dec 11, 2017, 8:01:03 PM)

1. Some facts on the Mangoldt function — eberlm <eberlm@in.tum.de> / hgweb

#1336 (Dec 9, 2017, 8:10:05 AM)

1. dedicated theory for group closure — haftmann / hgweb

#1335 (Dec 8, 2017, 9:22:03 PM)

1. clarified error; — wenzelm / hgweb

#1334 (Dec 8, 2017, 5:40:03 PM)

1. removed somewhat pointless warning; — wenzelm / hgweb

#1333 (Dec 8, 2017, 3:34:02 PM)

1. uniform use of original theory; — wenzelm / hgweb
2. implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof; — wenzelm / hgweb

#1332 (Dec 8, 2017, 8:04:06 AM)

1. avoid smt proofs in distribution — haftmann / hgweb

#1331 (Dec 7, 2017, 10:21:18 PM)

1. more robust; — wenzelm / hgweb

#1330 (Dec 7, 2017, 8:37:08 PM)

1. merged — wenzelm / hgweb
2. clarified document preparation vs. skip_proofs; — wenzelm / hgweb

#1329 (Dec 7, 2017, 6:32:18 PM)

1. "important" annotations — nipkow / hgweb

#1328 (Dec 7, 2017, 3:55:02 PM)

1. canonical name — nipkow / hgweb

#1327 (Dec 7, 2017, 11:46:06 AM)

1. tuned output in isar-ref manual; — wenzelm / hgweb
2. obsolete (used to be part of old src/Pure/codegen.ML); — wenzelm / hgweb

#1326 (Dec 6, 2017, 10:22:08 PM)

1. just one session for bulky HOL-Analysis documents; — wenzelm / hgweb
2. more default tags; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. prefer control symbol antiquotations; — wenzelm / hgweb
5. more robust, e.g. when Sidekick produces multi-selection; — wenzelm / hgweb
6. prefer control symbol antiquotations; — wenzelm / hgweb
7. more embedded cartouche arguments;
   more uniform LaTeX output for control symbols; — wenzelm / hgweb
8. name mangling for Latex macros;
   tuned signature; — wenzelm / hgweb

#1325 (Dec 6, 2017, 4:23:17 PM)

1. removed (un)important tags again to make latex happy — nipkow / hgweb

#1324 (Dec 6, 2017, 3:25:02 PM)

1. initial version of Analysis document — nipkow / hgweb

#1323 (Dec 6, 2017, 9:19:06 AM)

1. tuned — nipkow / hgweb

#1322 (Dec 5, 2017, 8:07:04 PM)

1. merged — wenzelm / hgweb
2. more documentation; — wenzelm / hgweb
3. explicit tag for document commands: avoid implicit use of document_tags; — wenzelm / hgweb
4. system option for default command tags; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb

#1321 (Dec 5, 2017, 4:49:03 PM)

1. Moved material from AFP to Analysis/Number_Theory — Manuel Eberl <eberlm@in.tum.de> / hgweb

#1320 (Dec 4, 2017, 11:49:47 PM)

1. merged — wenzelm / hgweb
2. NEWS; — wenzelm / hgweb
3. added action to make antiquoted cartouche; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. added GUI_Thread.future (similar to JFX_GUI.Thread.future): useful for experimentation with Scala console in Isabelle/jEdit; — wenzelm / hgweb
7. clarified control style; — wenzelm / hgweb
8. font style for literal control symbols, notably for antiquotations; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. tuned comments; — wenzelm / hgweb

#1319 (Dec 4, 2017, 9:34:02 PM)

1. more lemmas — nipkow / hgweb

#1318 (Dec 3, 2017, 10:40:05 PM)

1. misc tuning and modernization; — wenzelm / hgweb
2. simplified session (again, see 39e29972cb96): WordExamples requires < 1s; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. misc tuning and modernization; — wenzelm / hgweb

#1317 (Dec 3, 2017, 4:37:03 PM)

1. discontinued old 'def' command; — wenzelm / hgweb

#1316 (Dec 2, 2017, 8:22:06 PM)

1. more simplification rules — haftmann / hgweb
2. overhauling of primes — haftmann / hgweb
3. cleaned up and tuned — haftmann / hgweb
4. generalized more lemmas — haftmann / hgweb

#1315 (Dec 1, 2017, 9:16:06 PM)

1. tuned output; — wenzelm / hgweb
2. more operations; — wenzelm / hgweb
3. removed inaccessible blobs from Document.Nodes; — wenzelm / hgweb
4. more accurate JSON parsing according to http://seriot.ch/parsing_json.php — wenzelm / hgweb
5. purge hidden nodes more thoroughly: is_hidden may become true only later; — wenzelm / hgweb
6. proper synchronized Map: this may be used on multiple threads; — wenzelm / hgweb

#1314 (Dec 1, 2017, 9:34:01 AM)

1. bij_betw lemma for prime powers — eberlm <eberlm@in.tum.de> / hgweb
2. Existence of a holomorphic logarithm — eberlm <eberlm@in.tum.de> / hgweb

#1313 (Nov 29, 2017, 1:46:04 PM)

1. tuned; — wenzelm / hgweb
2. clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform; — wenzelm / hgweb
3. clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a); — wenzelm / hgweb

#1312 (Nov 27, 2017, 5:19:05 PM)

1. clarified description for mixed Mavericks / El Capitan system; — wenzelm / hgweb
2. updated documentation; — wenzelm / hgweb
3. prefer formal $POLYML_EXE; — wenzelm / hgweb
4. clarified main sessions; — wenzelm / hgweb
5. updated to official release of polyml-5.7.1;
   back to more modest default heap: e.g. relevant for Pure session for ML IDE;
   more robust POLYML_EXE; — wenzelm / hgweb
6. suppress warning; — wenzelm / hgweb
7. retain files in Pure.thy, notably $POLYML_EXE; — wenzelm / hgweb

#1311 (Nov 27, 2017, 11:58:04 AM)

1. proper context (as in 'term' command); — wenzelm / hgweb
2. proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit; — wenzelm / hgweb
3. more symbols; — wenzelm / hgweb
4. prefer Input.source (via cartouche); — wenzelm / hgweb
5. updated documentation: JVM is always 64bit; — wenzelm / hgweb

#1310 (Nov 26, 2017, 9:55:05 PM)

1. more symbols; — wenzelm / hgweb

#1309 (Nov 26, 2017, 1:52:03 PM)

1. clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps; — wenzelm / hgweb

#1308 (Nov 25, 2017, 3:31:06 PM)

1. macbroy2 is back, still pretending to be on Mavericks for better comparison of performance; — wenzelm / hgweb
2. Mac OS X 10.10 Yosemite is baseline; — wenzelm / hgweb

#1307 (Nov 24, 2017, 6:28:05 PM)

1. generalized more lemmas — haftmann / hgweb
2. tuned — haftmann / hgweb
3. tuned and generalized — haftmann / hgweb
4. tuned — haftmann / hgweb

#1306 (Nov 23, 2017, 2:13:05 PM)

1. new simp rule — haftmann / hgweb

#1305 (Nov 22, 2017, 12:13:03 PM)

1. Facts about complex n-th roots — eberlm <eberlm@in.tum.de> / hgweb

#1304 (Nov 21, 2017, 2:19:05 PM)

1. more lemmas — nipkow / hgweb

#1303 (Nov 19, 2017, 3:34:06 PM)

1. macbroy2 is inactive: system update; — wenzelm / hgweb

#1302 (Nov 17, 2017, 1:07:05 PM)

1. tuned — nipkow / hgweb

#1301 (Nov 16, 2017, 12:19:04 PM)

1. removed overambitious simp rules from e7e54a0b9197 — haftmann / hgweb

#1300 (Nov 14, 2017, 11:20:59 PM)

1. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
2. instantiation char :: full_exhaustive by Andreas Lochbihler — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1299 (Nov 14, 2017, 9:37:03 PM)

1. avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries; — wenzelm / hgweb
2. slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore (amending 2288cc39b038) — wenzelm / hgweb

#1298 (Nov 14, 2017, 4:51:32 PM)

1. merged — nipkow / hgweb
2. merged — nipkow / hgweb
3. tuned — nipkow / hgweb

#1297 (Nov 14, 2017, 3:49:07 PM)

1. removed pointless user_home: no measurable impact; — wenzelm / hgweb

#1296 (Nov 13, 2017, 3:19:05 PM)

1. init Mercurial repository for the generated session files; — wenzelm / hgweb
2. more operations; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. proper ssh.bash_path; — wenzelm / hgweb
5. more operations; — wenzelm / hgweb

#1295 (Nov 12, 2017, 9:40:06 PM)

1. synchronous use_theories, based on consolidated_state; — wenzelm / hgweb
2. clarified modules; — wenzelm / hgweb
3. optional session_base, e.g. from existing Sessions.Deps in build.scala; — wenzelm / hgweb
4. synchronous session start (similar to isabelle.vscode.Server); — wenzelm / hgweb
5. tuned signature (again, see 1a9e2a2bf251); — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. simplified: eliminated pointless Thy_Document_Model; — wenzelm / hgweb
8. theory nodes are never visible: avoid prints, which are not covered by node_consolidated; — wenzelm / hgweb
9. load theories via PIDE document update;
   theory nodes are always required; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. PIDE resources for theory files; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb

#1294 (Nov 11, 2017, 11:13:06 PM)

1. dedicated definition for coprimality — haftmann / hgweb
2. more induct rules on nat — haftmann / hgweb

#1293 (Nov 11, 2017, 7:52:05 PM)

1. avoid download of components; — wenzelm / hgweb
2. local user_home for improved performance, but only after given changeset for stability of measurement history; — wenzelm / hgweb
3. support alternative USER_HOME directory; — wenzelm / hgweb
4. clarified settings environment; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more options for "isabelle mkroot";
   updated documentation; — wenzelm / hgweb
8. adapted to changed ROOT syntax (see 13857f49d215);
   discontinued pointless option -d: always enabled; — wenzelm / hgweb
9. converted to Isabelle/Scala; — wenzelm / hgweb

#1292 (Nov 10, 2017, 10:13:03 PM)

1. replaced raw proof blocks by local lemmas — nipkow / hgweb

#1291 (Nov 9, 2017, 10:31:06 AM)

1. Replaced Raw Proof Blocks by Local Lemmas — nipkow / hgweb

#1290 (Nov 9, 2017, 9:16:05 AM)

1. tuned — nipkow / hgweb

#1289 (Nov 8, 2017, 9:10:05 PM)

1. merged — nipkow / hgweb
2. corrected priority — nipkow / hgweb

#1288 (Nov 8, 2017, 6:07:04 PM)

1. merged — wenzelm / hgweb
2. formal dependency on "poly" executable; — wenzelm / hgweb
3. removed obsolete workaround: always use existing IntInf.pow; — wenzelm / hgweb

#1287 (Nov 8, 2017, 3:37:08 PM)

1. strip some trailing spaces to force Pure rebuild after ce6454669360 — Lars Hupel <lars.hupel@mytum.de> / hgweb

#1286 (Nov 7, 2017, 10:16:05 PM)

1. merged — wenzelm / hgweb
2. proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc"; — wenzelm / hgweb
3. clarified signature (again); — wenzelm / hgweb
4. clarified exclusion: operate on completed selection, as last step; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. clarifified selection: always wrt. build_graph structure;
   tuned signature; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb

#1285 (Nov 7, 2017, 3:53:44 PM)

1. more robust parsing for THF proofs (esp. polymorphic Leo-III proofs) — blanchet / hgweb
2. integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch) — blanchet / hgweb
3. added FIXMEs — blanchet / hgweb

#1284 (Nov 7, 2017, 2:58:09 PM)

1. Replaced { } proofs by local lemmas; added Hoare logic with logical variables. — nipkow / hgweb

#1283 (Nov 7, 2017, 11:25:08 AM)

1. backed out odd "bug fix" 671decd2e627; — wenzelm / hgweb
2. more recent polyml-test version;
   afford more heap by default: all platforms are now 64bit and presumably have sufficient memory; — wenzelm / hgweb
3. minimal document model for theory files; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb

#1282 (Nov 6, 2017, 4:25:06 PM)

1. tuned signature; — wenzelm / hgweb

#1281 (Nov 5, 2017, 7:17:41 PM)

1. more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3); — wenzelm / hgweb

#1280 (Nov 5, 2017, 6:14:11 PM)

1. uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main"); — wenzelm / hgweb

#1279 (Nov 5, 2017, 4:31:05 PM)

1. updated comments; — wenzelm / hgweb
2. updated to scala-2.12.4; — wenzelm / hgweb

#1278 (Nov 5, 2017, 1:22:04 PM)

1. testing NewTestRegisterSave; — wenzelm / hgweb

#1277 (Nov 4, 2017, 10:45:00 PM)

1. superseded by plain_identify; — wenzelm / hgweb

#1276 (Nov 4, 2017, 8:59:09 PM)

1. tolerate odd negative times from old log files (before 1698e9ccef2d); — wenzelm / hgweb

#1275 (Nov 4, 2017, 7:40:04 PM)

1. prefer main entry points of HOL; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps; — wenzelm / hgweb

#1274 (Nov 4, 2017, 3:55:04 PM)

1. more robust sorted_entries; — wenzelm / hgweb
2. more convenient build_log_history; — wenzelm / hgweb

#1273 (Nov 4, 2017, 1:19:03 PM)

1. tuned; — wenzelm / hgweb
2. more portable print_time, notably for occasional negative (!) elapsed time of theory_timing; — wenzelm / hgweb
3. polyml-test version based on experimental branch NewTestRegisterSave; — wenzelm / hgweb

#1272 (Nov 3, 2017, 11:15:47 PM)

1. support for libgmp on x86_64-darwin; — wenzelm / hgweb

#1271 (Nov 3, 2017, 7:55:05 PM)

1. avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0; — wenzelm / hgweb
2. delegate boundary cases to existing IntInf.pow; — wenzelm / hgweb

#1270 (Nov 3, 2017, 5:37:05 PM)

1. plain identify job for Isabelle + AFP, independent of any Isabelle technology; — wenzelm / hgweb

#1269 (Nov 3, 2017, 2:16:04 PM)

1. tuned (non-unique example); — wenzelm / hgweb
2. clarified situation of global theory names; — wenzelm / hgweb
3. less global theories -- avoid confusion about special cases; — wenzelm / hgweb

#1268 (Nov 2, 2017, 3:31:04 PM)

1. proper deps; — wenzelm / hgweb

#1267 (Nov 2, 2017, 1:55:03 PM)

1. allow unrelated ancestor;
   clarified error; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. support alternative ancestor session; — wenzelm / hgweb
4. support focus_session, for much faster startup of Isabelle/jEdit;
   more options for "isabelle jedit"; — wenzelm / hgweb

#1266 (Nov 1, 2017, 10:46:52 PM)

1. more timing; — wenzelm / hgweb

#1265 (Nov 1, 2017, 9:49:07 PM)

1. tuned; — wenzelm / hgweb
2. init only once (see also c0f776b661fa); — wenzelm / hgweb
3. proper merge (amending fb46c031c841); — wenzelm / hgweb

#1264 (Nov 1, 2017, 6:53:01 PM)

1. build faster without heap images for minor imports; — wenzelm / hgweb
2. proper order for entries from multiple profiles, notably "AFP"; — wenzelm / hgweb

#1263 (Nov 1, 2017, 5:55:06 PM)

1. tuned output; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. logic_selector refers to raw logic name; — wenzelm / hgweb
4. clarified terminology; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. do not store bulky Session.Deps; — wenzelm / hgweb
7. avoid duplicate invocation of expensive Sessions.deps on full_sessions;
   tuned; — wenzelm / hgweb
8. added isabelle jedit options -B, -P, clarified -R;
   misc tuning and clarification; — wenzelm / hgweb

#1262 (Nov 1, 2017, 2:31:05 PM)

1. no heap sharing for empty session (e.g. HOL-ODE); — wenzelm / hgweb
2. tuned diagram; — wenzelm / hgweb
3. clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty; — wenzelm / hgweb

#1261 (Oct 31, 2017, 10:28:05 PM)

1. removed unused option, which is potentially expensive; — wenzelm / hgweb
2. allow to augment session context via explicit session infos;
   more compact required_session interface; — wenzelm / hgweb
3. synthesize session with all required theories from other session imports; — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. clarified signature: global_theories is always required; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. clarified modules; — wenzelm / hgweb
12. minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC; — wenzelm / hgweb
13. more permissive: db could be empty after hard crash; — wenzelm / hgweb
14. no censorship (in contrast to 2c828c830ad7); — wenzelm / hgweb

#1260 (Oct 31, 2017, 3:07:04 PM)

1. A few more topological results. And made some slow proofs faster — paulson <lp15@cam.ac.uk> / hgweb

#1259 (Oct 31, 2017, 8:31:05 AM)

1. removed ancient nat-int transfer — haftmann / hgweb
2. added lemma — haftmann / hgweb

#1258 (Oct 30, 2017, 10:58:48 PM)

1. added 'mlex_iff' lemma and simplified proof — blanchet / hgweb

#1257 (Oct 30, 2017, 9:10:57 PM)

1. merged — wenzelm / hgweb
2. recovered document from 9bfb6978eb80; — wenzelm / hgweb
3. NEWS; — wenzelm / hgweb
4. obsolete; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. ROOT cleanup: empty 'document_files' means there is no document; — wenzelm / hgweb
7. eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document; — wenzelm / hgweb
8. more informative timeout message, notably for build_status; — wenzelm / hgweb
9. clarified: adapted to ML version; — wenzelm / hgweb
10. proper order of initialization (amending 9953ae603a23); — wenzelm / hgweb

#1256 (Oct 30, 2017, 8:03:37 PM)

1. More topological results overlooked last time — paulson <lp15@cam.ac.uk> / hgweb

#1255 (Oct 30, 2017, 6:04:16 PM)

1. merged — paulson / hgweb
2. New results in topology, mostly from HOL Light's moretop.ml — paulson <lp15@cam.ac.uk> / hgweb

#1254 (Oct 30, 2017, 2:49:05 PM)

1. generalized some lemmas on multisets — haftmann / hgweb
2. rule out pathologic instances — haftmann / hgweb
3. tuned some proofs and added some lemmas — haftmann / hgweb

#1253 (Oct 29, 2017, 8:28:03 PM)

1. more recent polyml-test version; — wenzelm / hgweb

#1252 (Oct 29, 2017, 7:52:03 AM)

1. reduced simp_depth_limit — nipkow / hgweb

#1251 (Oct 29, 2017, 1:55:06 AM)

1. generalized — immler / hgweb

#1250 (Oct 28, 2017, 9:37:04 PM)

1. reduced heap hierarchy, for potentially improved performance; — wenzelm / hgweb

#1249 (Oct 28, 2017, 6:59:58 PM)

1. deactivated old tests; — wenzelm / hgweb

#1248 (Oct 28, 2017, 4:31:06 PM)

1. avoid slow proofs due to simp rules from 960509bfd47e; — wenzelm / hgweb

#1247 (Oct 27, 2017, 5:22:05 PM)

1. some concrete commands;
   clarified messages; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. more formal messages; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON; — wenzelm / hgweb
6. more permissive; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. separate JSON lexer; — wenzelm / hgweb
9. clarified command language; — wenzelm / hgweb

#1246 (Oct 26, 2017, 2:25:04 PM)

1. use Poly/ML 5.7.1 test version as default; — wenzelm / hgweb

#1245 (Oct 25, 2017, 3:13:06 PM)

1. more explicit check; — wenzelm / hgweb
2. more robust treatment of UTF8 in raw byte sources; — wenzelm / hgweb
3. clarified check, assuming that load commands are plain ASCII; — wenzelm / hgweb
4. more documentation; — wenzelm / hgweb
5. disallow blanks, relevant for session_name / theory_name e.g. in build log files; — wenzelm / hgweb
6. uniform system name; — wenzelm / hgweb

#1244 (Oct 24, 2017, 10:33:04 PM)

1. store session sources stamp; — wenzelm / hgweb

#1243 (Oct 24, 2017, 7:24:23 PM)

1. generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen — immler / hgweb

#1242 (Oct 24, 2017, 5:58:02 PM)

1. misc tuning and modernization; — wenzelm / hgweb
2. tuned output; — wenzelm / hgweb

#1241 (Oct 23, 2017, 9:52:13 PM)

1. discontinued Linux 32bit platform support; — wenzelm / hgweb
2. obsolete; — wenzelm / hgweb

#1240 (Oct 23, 2017, 8:52:03 PM)

1. merged — wenzelm / hgweb
2. updated to jdk-8u152, which is for x86_64 only; — wenzelm / hgweb

#1239 (Oct 23, 2017, 5:16:04 PM)

1. added lemma — nipkow / hgweb

#1238 (Oct 23, 2017, 2:22:04 PM)

1. minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC; — wenzelm / hgweb

#1237 (Oct 22, 2017, 10:34:03 PM)

1. tuned output; — wenzelm / hgweb

#1236 (Oct 22, 2017, 5:13:06 PM)

1. updated test version; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. auto update; — wenzelm / hgweb
4. more recent polyml-test version; — wenzelm / hgweb
5. parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs); — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned: build hg_graph only once;
   tuned signature; — wenzelm / hgweb

#1235 (Oct 22, 2017, 1:19:05 PM)

1. tuned — nipkow / hgweb
2. derived axiom iffI as a lemma (thanks to Alexander Maletzky) — nipkow / hgweb

#1234 (Oct 21, 2017, 9:43:03 PM)

1. remove trailing whitespaces in List — bulwahn / hgweb
2. drop a superfluous assumption that was found by the find_unused_assms command — bulwahn / hgweb
3. drop a superfluous assumption that was found by the find_unused_assms command and tune proof — bulwahn / hgweb
4. drop a superfluous assumption that was found by the find_unused_assms command and tune proof — bulwahn / hgweb

#1233 (Oct 21, 2017, 9:49:05 AM)

1. algebraic foundation for congruences — haftmann / hgweb

#1232 (Oct 21, 2017, 12:33:36 AM)

1. more ambitious test; — wenzelm / hgweb

#1231 (Oct 20, 2017, 9:04:05 PM)

1. added lemmas and tuned proofs — haftmann / hgweb

#1230 (Oct 20, 2017, 12:28:07 PM)

1. merged — paulson / hgweb
2. Switching to inverse image and constant_on, plus some new material — paulson <lp15@cam.ac.uk> / hgweb

#1229 (Oct 19, 2017, 1:04:06 AM)

1. proper integer option for Admin/build_history; — wenzelm / hgweb

#1228 (Oct 18, 2017, 8:37:05 PM)

1. clarified output; — wenzelm / hgweb
2. tuned output; — wenzelm / hgweb
3. more thorough treatment of afp_version and afp_pull_date; — wenzelm / hgweb

#1227 (Oct 18, 2017, 12:01:06 PM)

1. tuned options; — wenzelm / hgweb

#1226 (Oct 17, 2017, 2:13:04 PM)

1. tuned output; — wenzelm / hgweb
2. uniform execute, with proper isabelle_identifier (notably for "isabelle components -I"); — wenzelm / hgweb
3. tuned; — wenzelm / hgweb

#1225 (Oct 17, 2017, 11:40:03 AM)

1. permissive theory_timings for historic versions; — wenzelm / hgweb

#1224 (Oct 16, 2017, 9:04:02 PM)

1. store theory timings in session in build_log database;
   tuned; — wenzelm / hgweb
2. provide theory timing information, similar to command timing but always considered relevant; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. init user settings on fresh test machine; — wenzelm / hgweb

#1223 (Oct 16, 2017, 10:46:06 AM)

1. added [simp] — nipkow / hgweb

#1222 (Oct 15, 2017, 9:48:08 PM)

1. proper value; — wenzelm / hgweb

#1221 (Oct 15, 2017, 8:49:03 PM)

1. more AFP tests; — wenzelm / hgweb
2. added ml_statistics_step to trim stored properties; — wenzelm / hgweb

#1220 (Oct 15, 2017, 6:46:03 PM)

1. proper argument; — wenzelm / hgweb

#1219 (Oct 14, 2017, 10:25:03 PM)

1. tuned (graph.all_succs already contains origin); — wenzelm / hgweb
2. support for AFP versions;
   added AFP tests: non-slow, two partitions; — wenzelm / hgweb
3. clarified afp_pull_date: both repository versions are relevant; — wenzelm / hgweb
4. clarified stored build_args; — wenzelm / hgweb
5. partition AFP sessions according to structure, which happens to cut it roughly into equal parts; — wenzelm / hgweb
6. support for AFP in build_history and remote_build_history; — wenzelm / hgweb
7. tuned whitespace; — wenzelm / hgweb
8. support for AFP versions; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. support for AFP versions; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb

#1218 (Oct 13, 2017, 9:07:05 AM)

1. added lemmas, tuned spaces — nipkow / hgweb

#1217 (Oct 12, 2017, 9:40:05 PM)

1. entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless; — wenzelm / hgweb
2. more informative Imports.Report with actual session imports (minimized); — wenzelm / hgweb
3. more robust: allow URLs; — wenzelm / hgweb
4. more robust: allow Windows file names; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb

#1216 (Oct 12, 2017, 8:22:03 AM)

1. relaxed assm — nipkow / hgweb

#1215 (Oct 11, 2017, 11:11:11 PM)

1. back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50); — wenzelm / hgweb
2. reactivated unfinished tool (cf. a3a847c4fbdb); — wenzelm / hgweb

#1214 (Oct 11, 2017, 9:19:05 PM)

1. tuned whitespace; — wenzelm / hgweb
2. clarified meta_digest; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. added isablle build option -f; — wenzelm / hgweb

#1213 (Oct 11, 2017, 7:58:07 AM)

1. canonical multiplicative euclidean size — haftmann / hgweb
2. clarified parity — haftmann / hgweb
3. clarified uniqueness criterion for euclidean rings — haftmann / hgweb
4. tuned proofs — haftmann / hgweb
5. tuned imports — haftmann / hgweb

#1212 (Oct 10, 2017, 11:30:14 PM)

1. fixed markup — paulson <lp15@cam.ac.uk> / hgweb

#1211 (Oct 10, 2017, 8:39:49 PM)

1. ignore isolated nodes by default; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. cycle check with informative error; — wenzelm / hgweb
4. tuned: each session has at most one defining entry; — wenzelm / hgweb
5. more operations; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. tuned signature; — wenzelm / hgweb

#1210 (Oct 10, 2017, 6:22:08 PM)

1. Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems — paulson <lp15@cam.ac.uk> / hgweb

#1209 (Oct 10, 2017, 3:10:07 PM)

1. Session HOL-Analysis: Moebius functions and the Riemann mapping theorem. — paulson <lp15@cam.ac.uk> / hgweb

#1208 (Oct 10, 2017, 1:33:32 AM)

1. merged — wenzelm / hgweb
2. tuned: less oo-non-sense; — wenzelm / hgweb
3. operations for graph display; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. dependencies of entries vs. sessions;
   json output like "isabelle afp_dependencies";
   misc tuning; — wenzelm / hgweb
6. some administrative support for AFP; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. clarified signature: public access to ROOT file syntax; — wenzelm / hgweb

#1207 (Oct 9, 2017, 7:18:49 PM)

1. euclidean rings need no normalization — haftmann / hgweb
2. more fundamental definition of div and mod on int — haftmann / hgweb
3. one uniform type class for parity structures — haftmann / hgweb
4. generalized some rules — haftmann / hgweb
5. avoid variant of mk_sum — haftmann / hgweb
6. adjusted implementation according to comment — haftmann / hgweb
7. dropped duplicates — haftmann / hgweb
8. generalized simproc — haftmann / hgweb
9. replaced recdef were easy to replace — haftmann / hgweb
10. elementary definition of division on natural numbers — haftmann / hgweb
11. tuned structure — haftmann / hgweb
12. abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel — haftmann / hgweb
13. Polynomial_Factorial does not depend on Field_as_Ring as such — haftmann / hgweb
14. avoid name clashes on interpretation of abstract locales — haftmann / hgweb
15. avoid trivial definition — haftmann / hgweb
16. canonical introduction and destruction rules for pairwise — haftmann / hgweb
17. avoid fact name clashes — haftmann / hgweb
18. spelling and tuned whitespace — haftmann / hgweb
19. tuned — haftmann / hgweb
20. fundamental property of division by units — haftmann / hgweb
21. removed mere toy example from library — haftmann / hgweb
22. tuned proofs — haftmann / hgweb
23. dropped dead code — haftmann / hgweb
24. Fixed the theorem name "closed_imp_fip_compact" — paulson <lp15@cam.ac.uk> / hgweb

#1206 (Oct 9, 2017, 4:40:07 PM)

1. new material about connectedness, etc. — paulson <lp15@cam.ac.uk> / hgweb

#1205 (Oct 8, 2017, 5:00:26 PM)

1. more on Docker; — wenzelm / hgweb

#1204 (Oct 8, 2017, 4:01:05 PM)

1. removed obsolete RC tags; — wenzelm / hgweb
2. build_docker is regular tool (non-admin); — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. Added tag Isabelle2017 for changeset 64b47495676d — wenzelm / hgweb
5. obsolete; — wenzelm / hgweb
6. more NEWS; — wenzelm / hgweb
7. updated for release; — wenzelm / hgweb

#1203 (Oct 8, 2017, 2:07:04 PM)

1. merged — wenzelm / hgweb
2. proper File.platform_path for SML/NJ on Windows; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. proper output of raw ML; — wenzelm / hgweb

#1202 (Oct 7, 2017, 8:49:05 PM)

1. theory qualifier is always session name (see also 31e8a86971a8); — wenzelm / hgweb
2. clarified session structure; — wenzelm / hgweb

#1201 (Oct 7, 2017, 3:43:04 PM)

1. discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. clarified empty merge;
   tuned; — wenzelm / hgweb
4. permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make; — wenzelm / hgweb
5. prefer native platform x86-windows, to make this work on x86_64-cygwin; — wenzelm / hgweb

#1200 (Oct 6, 2017, 10:01:06 PM)

1. tuned signature; — wenzelm / hgweb
2. even more robust syntax (amending 122df1fde073); — wenzelm / hgweb
3. clarified error for bad session-qualified imports; — wenzelm / hgweb
4. clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header; — wenzelm / hgweb

#1199 (Oct 5, 2017, 6:07:06 PM)

1. merged — wenzelm / hgweb
2. completion supports theory header imports;
   tuned; — wenzelm / hgweb
3. clarified modules; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb

#1198 (Oct 5, 2017, 4:43:05 PM)

1. new theorem at_within_cbox_finite — paulson <lp15@cam.ac.uk> / hgweb

#1197 (Oct 4, 2017, 9:28:03 PM)

1. process ROOT files only once, which allows duplicate (or overlapping) session root directories; — wenzelm / hgweb

#1196 (Oct 3, 2017, 8:57:39 PM)

1. prefer Cygwin64, although some components still require update; — wenzelm / hgweb

#1195 (Oct 3, 2017, 7:16:05 PM)

1. updated test version; — wenzelm / hgweb
2. more recent polyml-test version; — wenzelm / hgweb

#1194 (Oct 3, 2017, 1:01:15 AM)

1. misc tuning and modernization; — wenzelm / hgweb

#1193 (Oct 2, 2017, 9:31:09 PM)

1. discontinued obsolete 'files' in session ROOT; — wenzelm / hgweb
2. prefer file dependencies wrt. specific theories; — wenzelm / hgweb
3. added command 'external_file'; — wenzelm / hgweb
4. proper document (cf. 9f5bfef8bd82); — wenzelm / hgweb
5. removed pointless dependencies: done by 'spark_open'; — wenzelm / hgweb

#1192 (Oct 2, 2017, 5:16:08 PM)

1. merged — wenzelm / hgweb
2. more documentation; — wenzelm / hgweb
3. clarified imports: prefer parent session images; — wenzelm / hgweb
4. eliminated old-style no-document imports; — wenzelm / hgweb
5. proper document; — wenzelm / hgweb
6. more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions; — wenzelm / hgweb
7. more documentation; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. sources_stamp refers to full sources;
   simplified data storage (again); — wenzelm / hgweb
10. option -S for "isabelle build"; — wenzelm / hgweb
11. persistent storage of imported_sources; — wenzelm / hgweb
12. cache sources: invoke SHA1.digest at most once;
    maintain imported_sources, as required for new theories; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb

#1191 (Oct 2, 2017, 4:04:06 AM)

1. repaired small incident — blanchet / hgweb

#1190 (Oct 1, 2017, 3:25:03 PM)

1. updated SMT certificates and added one test — blanchet / hgweb
2. updated NEWS — blanchet / hgweb
3. properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly) — blanchet / hgweb

#1189 (Oct 1, 2017, 1:19:03 PM)

1. option -B for "isabelle build" and "isabelle imports"; — wenzelm / hgweb
2. more standard merge operation; — wenzelm / hgweb

#1188 (Sep 30, 2017, 11:13:11 PM)

1. updated Sledgehammer docs — blanchet / hgweb
2. added veriT component — blanchet / hgweb

#1187 (Sep 30, 2017, 8:25:06 PM)

1. more and updated documentation; — wenzelm / hgweb
2. more and updated documentation; — wenzelm / hgweb
3. discontinued rudiments of BSD support;
   tuned comments; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb

#1186 (Sep 30, 2017, 1:22:10 PM)

1. NEWS; — wenzelm / hgweb
2. x86-cygwin for tools is no longer supported; — wenzelm / hgweb
3. updated to x86_64-cygwin; — wenzelm / hgweb
4. updated to x86_64-cygwin; — wenzelm / hgweb
5. auto update; — wenzelm / hgweb
6. "windows" application is always x86_64; — wenzelm / hgweb

#1185 (Sep 29, 2017, 11:07:04 PM)

1. merged — wenzelm / hgweb
2. unused; — wenzelm / hgweb
3. more accurate node_syntax: avoid overall_syntax for PIDE edits; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. clarified theory syntax vs. overall session syntax; — wenzelm / hgweb
6. unused; — wenzelm / hgweb
7. more informative loaded_theories: dependencies and syntax; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. session-qualified theory names are mandatory; — wenzelm / hgweb
13. discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this; — wenzelm / hgweb

#1184 (Sep 29, 2017, 6:54:03 PM)

1. eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen — paulson <lp15@cam.ac.uk> / hgweb

#1183 (Sep 29, 2017, 4:58:03 PM)

1. Merge (resolved trivial conflict) — paulson <lp15@cam.ac.uk> / hgweb
2. New results for Green's theorem — paulson <lp15@cam.ac.uk> / hgweb

#1182 (Sep 28, 2017, 9:58:02 PM)

1. merged — paulson / hgweb
2. merged — paulson / hgweb
3. merged — paulson / hgweb
4. merged — paulson / hgweb
5. more proof simplificaition — paulson <lp15@cam.ac.uk> / hgweb

#1181 (Sep 28, 2017, 10:25:06 AM)

1. merged — wenzelm / hgweb
2. maintain loaded_files for each theory; — wenzelm / hgweb
3. clarified: more uniform results; — wenzelm / hgweb
4. slightly more parallelism; — wenzelm / hgweb
5. prefer sequential file-system access, but parallel parse; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. clarified pure_files, based on uniform loaded_files; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. tuned signature -- more readable output as Scala value; — wenzelm / hgweb
10. more operations; — wenzelm / hgweb

#1180 (Sep 26, 2017, 9:31:07 PM)

1. strengthened reconstruction tactic — blanchet / hgweb

#1179 (Sep 25, 2017, 9:04:05 PM)

1. basic support for x86_64-cygwin; — wenzelm / hgweb

#1178 (Sep 25, 2017, 4:55:04 PM)

1. Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen — paulson <lp15@cam.ac.uk> / hgweb

#1177 (Sep 25, 2017, 9:55:05 AM)

1. back to post-release mode;
   updated package; — wenzelm / hgweb