SuccessChanges

Summary

  1. tuned
  2. merged
  3. tuned;
  4. clarified theory status;
  5. dump ZF in parallel to HOL Main;
  6. tuned messages;
  7. more ambitious options (again);
  8. more ambitious options (again, after 93aa546ffbac);
  9. tuned signature;
  10. proper clean_theories wrt. dynamic dep_graph;
  11. tuned signature;
  12. potentially more robust: read under lock if not yet set;
  13. tuned;
  14. New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
  15. session directories need to exist;
  16. clarified signature: eliminated unused option;
  17. merged
  18. importation fix
  19. merged
  20. new material on Analysis, plus some rearrangements
  21. eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f);
  22. discontinued obsolete "isabelle imports" and all_known data;
  23. avoid duplicate directories wrt. synthetic session;
  24. disallow accidental duplicates within the same session specification -- proper total match;
  25. find theory files via session structure: much faster Prover IDE startup;
  26. find theory node name via session directories;
  27. disallow overlapping session directories;
  28. tidied up some massive ugliness
  29. clarified messages;
  30. clarified syntax: 'directories' and 'theories' belong together;
  31. more documentation;
  32. check session directories;
  33. declare session directories;
  34. clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
  35. theory_name based on session_directories: no need for expensive all_known;
  36. clarified session_directories: relative to session_path, with overlapping information;
  37. clarified signature: retain global session information, unaffected by later restriction;
  38. disable fragile options for now;
  39. avoid overlapping session directories;
  40. support for explicit session directories;
  41. obsolete (see 94442fce40a5);
  42. optional trace output;
  43. prefer commands_accepted: fewer protocol messages;
  44. prefer define_commands_bulk: fewer protocol messages;
  45. clarified signature;
  46. tuned signature -- prefer bulk messages;
  47. tuned signature;
  48. proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
  49. more robust;
  50. unused;
  51. proper finished_theory status for result;
  52. more central checkpoint;
  53. disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;
  54. merged
  55. load theories in stages, to reduce ML heap requirements;
  56. more complete graph;
  57. tuned messages;
  58. tuned signature;
  59. clarified signature;
  60. tuned important special case;
  61. tuned signature;
  62. more dump_checkpoints;
  63. clarified signature;
  64. clarified state variable: avoid extra mutability via Promise;
  65. Removal of the redundant ancestor Continuous_Extension
  66. Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
  67. Theory Derivative no longer depends on Path_Connected
  68. more explicit type Dump.Session, with context information;
  69. proper orientation;
  70. clarified signature: prefer operations without position;
  71. prefer Theory_Ordering theory names are unique (due to proper session context);
  72. clarified signature: full dependency graph;
  73. merged
  74. more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
  75. tuned signature;
  76. merged
  77. more rules for ordered real vector spaces
  78. simplified proofs
  79. simplified setup
  80. tuned proof
  81. merged
  82. enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;
  83. support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
  84. more scalable -- less ML heap requirements;
  85. tuned whitespace;
  86. Integrate locale activation fallback diagnostics with 'trace_locales'.
Changeset 70897:3e11f35496b3 by nipkow:
tuned
The file was modifiedsrc/HOL/Data_Structures/RBT_Map.thy (diff)
The file was modifiedsrc/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modifiedsrc/HOL/Data_Structures/Set2_Join_RBT.thy (diff)
Changeset 70896:374caac3d624 by wenzelm:
merged
Changeset 70895:437da7b72b5e by wenzelm:
tuned;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70894:b080d1fb9777 by wenzelm:
clarified theory status;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70893:edd856e6051a by wenzelm:
dump ZF in parallel to HOL Main;
The file was modifiedsrc/ZF/ROOT (diff)
Changeset 70892:a65b9624cb98 by wenzelm:
tuned messages;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70891:e54213954efc by wenzelm:
more ambitious options (again);
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70890:4b3cfd73f428 by wenzelm:
more ambitious options (again, after 93aa546ffbac);
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70889:3eb30d80cee6 by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/General/graph.scala (diff)
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70888:93aa546ffbac by wenzelm:
proper clean_theories wrt. dynamic dep_graph;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70887:43bdcf778cfe by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70886:47ca5c7550e4 by wenzelm:
potentially more robust: read under lock if not yet set;
The file was modifiedsrc/Pure/Concurrent/single_assignment.ML (diff)
Changeset 70885:5d32cca55c2a by wenzelm:
tuned;
The file was modifiedsrc/Pure/PIDE/document.ML (diff)
Changeset 70884:ae37b8fbf023 by paulson <lp15@cam.ac.uk>:
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
The file was addedsrc/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
The file was modifiedsrc/HOL/Analysis/Analysis.thy (diff)
The file was modifiedsrc/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modifiedsrc/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modifiedsrc/HOL/Limits.thy (diff)
Changeset 70883:0fec12eabad0 by wenzelm:
session directories need to exist;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70882:41b5e515c238 by wenzelm:
clarified signature: eliminated unused option;
The file was modifiedsrc/Pure/General/graph.scala (diff)
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
Changeset 70881:7e93a10b21f0 by paulson:
merged
Changeset 70880:8518a750f7bb by paulson <lp15@cam.ac.uk>:
importation fix
The file was modifiedsrc/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
Changeset 70879:67360d50ebb3 by paulson:
merged
Changeset 70878:3d894e1cfc75 by paulson <lp15@cam.ac.uk>:
new material on Analysis, plus some rearrangements
The file was modifiedsrc/HOL/Analysis/Borel_Space.thy (diff)
The file was modifiedsrc/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modifiedsrc/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modifiedsrc/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modifiedsrc/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modifiedsrc/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modifiedsrc/HOL/Library/Landau_Symbols.thy (diff)
The file was modifiedsrc/HOL/Limits.thy (diff)
The file was modifiedsrc/HOL/Power.thy (diff)
The file was modifiedsrc/HOL/Probability/Tree_Space.thy (diff)
Changeset 70877:086575316fd5 by wenzelm:
eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f);
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70876:9cde8c4ea5a5 by wenzelm:
discontinued obsolete &quot;isabelle imports&quot; and all_known data;
The file was modifiedNEWS (diff)
The file was modifiedsrc/Doc/System/Sessions.thy (diff)
The file was modifiedsrc/Pure/System/isabelle_tool.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/build-jars (diff)
The file was removedsrc/Pure/Tools/imports.scala
Changeset 70875:c1597167563e by wenzelm:
avoid duplicate directories wrt. synthetic session;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70874:60b1eda998f3 by wenzelm:
disallow accidental duplicates within the same session specification -- proper total match;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70873:8c7706b053c7 by wenzelm:
find theory files via session structure: much faster Prover IDE startup;
The file was modifiedNEWS (diff)
The file was modifiedsrc/Doc/JEdit/JEdit.thy (diff)
The file was modifiedsrc/Pure/ML/ml_process.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/PIDE/protocol.ML (diff)
The file was modifiedsrc/Pure/PIDE/protocol.scala (diff)
The file was modifiedsrc/Pure/PIDE/resources.ML (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.ML (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Tools/build.ML (diff)
The file was modifiedsrc/Pure/Tools/build.scala (diff)
The file was modifiedsrc/Pure/Tools/imports.scala (diff)
The file was modifiedsrc/Tools/VSCode/src/server.scala (diff)
The file was modifiedsrc/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modifiedsrc/Tools/jEdit/lib/Tools/jedit (diff)
The file was modifiedsrc/Tools/jEdit/src/jedit_resources.scala (diff)
The file was modifiedsrc/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 70872:4c53227f4b73 by wenzelm:
find theory node name via session directories;
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modifiedsrc/Tools/jEdit/src/jedit_resources.scala (diff)
Changeset 70871:a6c0f2d106c8 by wenzelm:
disallow overlapping session directories;
The file was modifiedNEWS (diff)
The file was modifiedsrc/Doc/System/Sessions.thy (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Sessions.thy (diff)
The file was modifiedsrc/Pure/Thy/sessions.ML (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70870:b8cd7ea34e33 by paulson <lp15@cam.ac.uk>:
tidied up some massive ugliness
The file was modifiedsrc/HOL/Library/Permutation.thy (diff)
Changeset 70869:7b6e6d61204a by wenzelm:
clarified messages;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70868:36c8c32346cb by wenzelm:
clarified syntax: &#039;directories&#039; and &#039;theories&#039; belong together;
The file was modifiedsrc/CCL/ROOT (diff)
The file was modifiedsrc/CTT/ROOT (diff)
The file was modifiedsrc/Doc/ROOT (diff)
The file was modifiedsrc/Doc/System/Sessions.thy (diff)
The file was modifiedsrc/HOL/ROOT (diff)
The file was modifiedsrc/LCF/ROOT (diff)
The file was modifiedsrc/Pure/Thy/sessions.ML (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70867:56d70f7ce4a4 by wenzelm:
more documentation;
The file was modifiedNEWS (diff)
The file was modifiedsrc/Doc/System/Sessions.thy (diff)
Changeset 70866:73812c598a26 by wenzelm:
check session directories;
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70865:efd995488228 by wenzelm:
declare session directories;
The file was modifiedsrc/CCL/ROOT (diff)
The file was modifiedsrc/CTT/ROOT (diff)
The file was modifiedsrc/Doc/ROOT (diff)
The file was modifiedsrc/FOL/ROOT (diff)
The file was modifiedsrc/HOL/ROOT (diff)
The file was modifiedsrc/LCF/ROOT (diff)
The file was modifiedsrc/Sequents/ROOT (diff)
Changeset 70864:29bb1ebb188f by wenzelm:
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70863:b0172698d0d3 by wenzelm:
theory_name based on session_directories: no need for expensive all_known;
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70862:e4bba654d085 by wenzelm:
clarified session_directories: relative to session_path, with overlapping information;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70861:cb1776c8e216 by wenzelm:
clarified signature: retain global session information, unaffected by later restriction;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Tools/build.scala (diff)
Changeset 70860:a1dfd603260e by wenzelm:
disable fragile options for now;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70859:abdf3732f6f1 by wenzelm:
avoid overlapping session directories;
The file was modifiedsrc/HOL/ROOT (diff)
Changeset 70858:9cac4dec0da9 by wenzelm:
support for explicit session directories;
The file was modifiedsrc/Pure/Isar/parse.scala (diff)
The file was modifiedsrc/Pure/Sessions.thy (diff)
The file was modifiedsrc/Pure/Thy/sessions.ML (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70857:3cab8dad5b40 by wenzelm:
obsolete (see 94442fce40a5);
The file was modifiedsrc/Tools/Haskell/Haskell.thy (diff)
Changeset 70856:e56ec28fc5e8 by wenzelm:
optional trace output;
The file was modifiedsrc/Pure/PIDE/prover.scala (diff)
Changeset 70855:94442fce40a5 by wenzelm:
prefer commands_accepted: fewer protocol messages;
The file was modifiedsrc/Pure/PIDE/document.ML (diff)
The file was modifiedsrc/Pure/PIDE/markup.ML (diff)
The file was modifiedsrc/Pure/PIDE/markup.scala (diff)
The file was modifiedsrc/Pure/PIDE/protocol.ML (diff)
The file was modifiedsrc/Pure/PIDE/protocol.scala (diff)
The file was modifiedsrc/Pure/PIDE/session.scala (diff)
Changeset 70854:2bd9e30183b1 by wenzelm:
prefer define_commands_bulk: fewer protocol messages;
The file was modifiedsrc/Pure/PIDE/protocol.ML (diff)
The file was modifiedsrc/Pure/PIDE/protocol.scala (diff)
The file was modifiedsrc/Pure/PIDE/session.scala (diff)
Changeset 70853:4a358f8c7cb7 by wenzelm:
clarified signature;
The file was modifiedsrc/Pure/PIDE/document.ML (diff)
The file was modifiedsrc/Pure/PIDE/protocol.ML (diff)
Changeset 70852:0f9a4e8ee1ab by wenzelm:
tuned signature -- prefer bulk messages;
The file was modifiedsrc/Pure/General/output.ML (diff)
The file was modifiedsrc/Pure/PIDE/command.ML (diff)
The file was modifiedsrc/Pure/PIDE/document.ML (diff)
The file was modifiedsrc/Pure/PIDE/execution.ML (diff)
Changeset 70851:9c4809ec28ef by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/PIDE/protocol.scala (diff)
The file was modifiedsrc/Pure/PIDE/prover.scala (diff)
The file was modifiedsrc/Pure/PIDE/session.scala (diff)
Changeset 70850:373d95cf1b98 by wenzelm:
proper session-qualifier imports (amending &quot;fixes&quot; from adaa0a6ea4fe);
The file was modifiedsrc/HOL/Algebra/Free_Abelian_Groups.thy (diff)
The file was modifiedsrc/HOL/ROOT (diff)
Changeset 70849:44588e355ca8 by wenzelm:
more robust;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70848:4655897b8287 by wenzelm:
unused;
The file was modifiedsrc/Pure/PIDE/document_status.scala (diff)
Changeset 70847:2bf1d0e57695 by wenzelm:
proper finished_theory status for result;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70846:774cc139b1f4 by wenzelm:
more central checkpoint;
The file was modifiedsrc/ZF/ROOT (diff)
Changeset 70845:f51955effb02 by wenzelm:
disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70844:cce7a95f6e0f by wenzelm:
merged
Changeset 70843:f7c5b30fc432 by wenzelm:
load theories in stages, to reduce ML heap requirements;
The file was modifiedsrc/Pure/PIDE/document_status.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70842:d5e4231caa06 by wenzelm:
more complete graph;
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
Changeset 70841:d1d4a1b1ff1f by wenzelm:
tuned messages;
The file was modifiedsrc/Pure/General/graph.scala (diff)
Changeset 70840:fa04b549f652 by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70839:9a40720750dc by wenzelm:
clarified signature;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70838:60cb2bfea2d2 by wenzelm:
tuned important special case;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70837:3047b7671279 by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70836:a4d265a6c5cc by wenzelm:
more dump_checkpoints;
The file was modifiedsrc/HOL/ROOT (diff)
Changeset 70835:fc27cecb66d8 by wenzelm:
clarified signature;
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70834:b23a6dfcfd57 by wenzelm:
clarified state variable: avoid extra mutability via Promise;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
Changeset 70833:93a7a85de312 by paulson <lp15@cam.ac.uk>:
Removal of the redundant ancestor Continuous_Extension
The file was modifiedsrc/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modifiedsrc/HOL/Analysis/Retracts.thy (diff)
Changeset 70832:de9c4ed2d5df by paulson <lp15@cam.ac.uk>:
Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
The file was addedsrc/HOL/Analysis/Retracts.thy
The file was modifiedsrc/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modifiedsrc/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modifiedsrc/HOL/Analysis/Further_Topology.thy (diff)
Changeset 70831:0e2a065d6f31 by paulson <lp15@cam.ac.uk>:
Theory Derivative no longer depends on Path_Connected
The file was modifiedsrc/HOL/Analysis/Derivative.thy (diff)
The file was modifiedsrc/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modifiedsrc/HOL/Analysis/Polytope.thy (diff)
Changeset 70830:5f4b8a505090 by wenzelm:
more explicit type Dump.Session, with context information;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
The file was modifiedsrc/Pure/Tools/update.scala (diff)
Changeset 70829:ad7891a73230 by wenzelm:
proper orientation;
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70828:f164cec7ac22 by wenzelm:
clarified signature: prefer operations without position;
The file was modifiedsrc/Pure/PIDE/command.scala (diff)
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/PIDE/protocol.scala (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Thy/thy_header.scala (diff)
The file was modifiedsrc/Pure/Thy/thy_syntax.scala (diff)
The file was modifiedsrc/Pure/Tools/imports.scala (diff)
Changeset 70827:4c98d37e1448 by wenzelm:
prefer Theory_Ordering theory names are unique (due to proper session context);
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70826:a56eab490f4e by wenzelm:
clarified signature: full dependency graph;
The file was modifiedsrc/Pure/General/graph.scala (diff)
The file was modifiedsrc/Pure/PIDE/document.scala (diff)
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
Changeset 70825:39c90514faf8 by wenzelm:
merged
Changeset 70824:0f8742b5a9e8 by wenzelm:
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
The file was modifiedetc/options (diff)
The file was modifiedsrc/HOL/ROOT (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/Thy/sessions.scala (diff)
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
The file was modifiedsrc/ZF/ROOT (diff)
Changeset 70823:b99b925dbd84 by wenzelm:
tuned signature;
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
Changeset 70822:f54b19ca9994 by nipkow:
merged
Changeset 70821:2402aa499ffe by haftmann:
more rules for ordered real vector spaces
The file was modifiedsrc/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modifiedsrc/HOL/Real_Vector_Spaces.thy (diff)
Changeset 70820:f14b997da756 by nipkow:
simplified proofs
The file was modifiedsrc/HOL/Data_Structures/List_Ins_Del.thy (diff)
The file was modifiedsrc/HOL/Data_Structures/Set_Specs.thy (diff)
Changeset 70819:2bbd945728e2 by nipkow:
simplified setup
The file was modifiedsrc/HOL/Data_Structures/List_Ins_Del.thy (diff)
Changeset 70818:40b63f2655e8 by nipkow:
tuned proof
The file was modifiedsrc/HOL/Data_Structures/Tree234_Set.thy (diff)
The file was modifiedsrc/HOL/Data_Structures/Tree23_Set.thy (diff)
Changeset 70817:e59a4ae35b88 by wenzelm:
merged
Changeset 70816:cb83a582bf0c by wenzelm:
enable share_common_data for &quot;isabelle dump&quot; and its derivatives (e.g. &quot;isabelle mmt_import&quot;): this has the potential to reduce ML heap size considerably, after initial command definitions;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70815:1ae987cc052f by wenzelm:
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
The file was modifiedsrc/Pure/PIDE/headless.scala (diff)
The file was modifiedsrc/Pure/PIDE/resources.scala (diff)
The file was modifiedsrc/Pure/PIDE/session.scala (diff)
The file was modifiedsrc/Pure/Thy/thy_syntax.scala (diff)
Changeset 70814:06052394efbe by wenzelm:
more scalable -- less ML heap requirements;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70813:44090b702e11 by wenzelm:
tuned whitespace;
The file was modifiedsrc/Pure/Tools/dump.scala (diff)
Changeset 70812:2fb2e7661e16 by ballarin:
Integrate locale activation fallback diagnostics with &#039;trace_locales&#039;.
The file was modifiedsrc/Pure/Isar/expression.ML (diff)
The file was modifiedsrc/Pure/Isar/locale.ML (diff)