- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Nov 26 2021
Nov 26 2021
clarified modules (see c299abcf7081);
makarius committed rISABELLEfe9e590ae52f: output for document commands like 'section', 'text' is defined in user-space….
output for document commands like 'section', 'text' is defined in user-space…
tuned signature: more explicit types for presentation;
more robust support for Windows line-endings;
makarius committed rISABELLEf31229171b3b: source positions for document markup commands, e.g. to retrieve PIDE markup in….
source positions for document markup commands, e.g. to retrieve PIDE markup in…
makarius committed rISABELLEc1b5d6e6ff74: clarified system option standard values: avoid oddities like "isabelle build -o….
clarified system option standard values: avoid oddities like "isabelle build -o…
makarius committed rISABELLE46c7fafbea3d: more compact data during presentation: Entity_Context.Theory_Export instead of….
more compact data during presentation: Entity_Context.Theory_Export instead of…
makarius committed rISABELLE0e4d8aa61ad7: more symbolic latex_output via XML (using YXML within text);.
more symbolic latex_output via XML (using YXML within text);
proper enclose_name (amending e77c5bfca9aa);
makarius committed rISABELLE6424f74fd9d4: Latex.Output.latex_heading depends on option document_heading_prefix, e.g..
Latex.Output.latex_heading depends on option document_heading_prefix, e.g.
makarius committed rISABELLEa1fa82431576: clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT….
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT…
more symbolic latex_output via XML;
updated to verit-2021.06.2-rmx;
makarius committed rISABELLE3064e165c660: clarified HTML_Context.theory_exports: prefer value-oriented parallelism;.
clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
makarius committed rISABELLEcfc15da73a78: afford more parallelism for sessions (instead of theories in 5eac4b13d1f1)….
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1)…
makarius committed rISABELLE1e7bb95c75e7: more parallelism, at the cost of potential duplicates of make_thy;.
more parallelism, at the cost of potential duplicates of make_thy;
generate problems with correct logic for veriT
makarius committed rISABELLE2ad892ac749a: present only selected session theories (as in Isabelle2021), in contrast to….
present only selected session theories (as in Isabelle2021), in contrast to…
tuned (see also e0d1d9203275);
clarified signature;
desharna committed rISABELLEb65336541c19: renamed multp_code_iff and multeqp_code_iff.
renamed multp_code_iff and multeqp_code_iff
desharna committed rISABELLEba59c691b3ee: added asymp_{less,greater} to preorder and moved mult1_lessE out.
added asymp_{less,greater} to preorder and moved mult1_lessE out
dcjm committed rPOLYML39d96a2def90: Fix Overflow exception packet in Real.toInt in the interpreter. Fixes #164. (authored by dcjm).
Fix Overflow exception packet in Real.toInt in the interpreter. Fixes #164.
desharna committed rISABELLE5749fefd3fa0: simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0.
simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0
Nov 25 2021
Nov 25 2021
Fabian Huch <huch@in.tum.de> committed rAFP5f2eb2ceef51: moved extraction of related entries to hugo;.
moved extraction of related entries to hugo;
desharna committed rISABELLE825cd198d85c: renamed Multiset.multp and Multiset.multeqp.
renamed Multiset.multp and Multiset.multeqp
Fabian Huch <huch@in.tum.de> committed rAFPcea71b734a23: added keywords to site generated entry data;.
added keywords to site generated entry data;
Fabian Huch <huch@in.tum.de> committed rAFPa53823fdccd8: improved keyword extraction;.
improved keyword extraction;
Fabian Huch <huch@in.tum.de> committed rAFPb69b09d8f99a: use tmp file for python script instead of command;.
use tmp file for python script instead of command;
Fabian Huch <huch@in.tum.de> committed rAFPe450d45c4680: added js-side theory loading to afp site;.
added js-side theory loading to afp site;
Nov 23 2021
Nov 23 2021
dcjm committed rPOLYML020d4d7b2831: Fix Overflow exception packet in Real.toInt in the interpreter. Fixes #164. (authored by dcjm).
Fix Overflow exception packet in Real.toInt in the interpreter. Fixes #164.
Nov 22 2021
Nov 22 2021
Fabian Huch <huch@in.tum.de> committed rAFP5857c4582eae: integrated metadata changes into site;.
integrated metadata changes into site;
Fabian Huch <huch@in.tum.de> committed rAFP09790a81f454: added missing keyword data;.
added missing keyword data;
Fabian Huch <huch@in.tum.de> committed rAFP5369b980e2fe: removed html dir from sitegen (now set inside hugo);.
removed html dir from sitegen (now set inside hugo);
Fabian Huch <huch@in.tum.de> committed rAFPc5355362ec54: tuned sitegen: moved dependencies generation to scala.
tuned sitegen: moved dependencies generation to scala
Fabian Huch <huch@in.tum.de> committed rAFPdf920a57d3cf: changed generated author format;.
changed generated author format;
Fabian Huch <huch@in.tum.de> committed rAFP2b9064e3aaa4: tuned hugo: static files more explicit;.
tuned hugo: static files more explicit;
Nov 17 2021
Nov 17 2021
paulson <lp15@cam.ac.uk> committed rAFP1fe98b11c666: A slightly stronger lemma allowing slightly simpler proofs.
A slightly stronger lemma allowing slightly simpler proofs
Fabian Huch <huch@in.tum.de> committed rAFPd7cd94262b1a: added missing name mapping to migration;.
added missing name mapping to migration;
Fabian Huch <huch@in.tum.de> committed rAFPf81257bb1f6d: clarified hugo data;.
clarified hugo data;
Fabian Huch <huch@in.tum.de> committed rAFP29324715b4d0: proper authors/affiliations gen for hugo taxonomy;.
proper authors/affiliations gen for hugo taxonomy;
Fabian Huch <huch@in.tum.de> committed rAFPa125cf87f609: proper output path;.
proper output path;
Nov 16 2021
Nov 16 2021
makarius committed rISABELLE3dfb8e47a6b7: removed redundant test (see also 86fac52c2795, a9fea3f11cc0);.
removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
makarius committed rISABELLE507f50dbeb79: just one Presentation.State for all sessions: avoid duplication of already….
just one Presentation.State for all sessions: avoid duplication of already…
makarius committed rISABELLE796ae338eb9d: back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in….
back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in…
makarius committed rISABELLE5eac4b13d1f1: less ambitious parallelism: more direct read/write saves overall heap space and….
less ambitious parallelism: more direct read/write saves overall heap space and…
updated NEWS: arm64-linux support is almost complete;
makarius committed rISABELLEc606fddc5b05: slightly faster XML output: avoid too much regrowing of StringBuilder;.
slightly faster XML output: avoid too much regrowing of StringBuilder;
more material for HOL-Analysis.Infinite_Sum
makarius committed rISABELLE87718883c8b9: update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux….
update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux…
more symbolic latex_output via XML;
updated to polyml-5.9-610a153b941d -- close to final;
clarified signature;
more symbolic latex output;
makarius committed rISABELLEf118008a8131: tuned signature (again): latex_output is likely to depend on context;.
tuned signature (again): latex_output is likely to depend on context;
makarius committed rISABELLEd2522bb4db1b: symbolic latex_output via XML, interpreted in Isabelle/Scala;.
symbolic latex_output via XML, interpreted in Isabelle/Scala;
clarified signature;
clarified signature;
tuned output --- less redundancy;
clarified signature: more privacy;
makarius committed rISABELLE2fd0c33fe440: clarified signature: Latex.Output as parameter to Document_Build.Engine;.
clarified signature: Latex.Output as parameter to Document_Build.Engine;
proper detection of ARM platform variants;
Dominique Unruh <unruh@ut.ee> committed rAFP5b1ae11ed404: Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now….
Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now…
paulson <lp15@cam.ac.uk> committed rAFP619663adf685: Elimination of all z3 calls.
Elimination of all z3 calls
Word_Lib sync from l4v; tweak word_eqI
generalise word_eqI method; make sure it is exercised
test_bit_size not longer needed; avoid potential nontermination
Word_Lib tweaks for slightly more backwards compatibility
use bit_simps in word_eqI method
adapted to new version of Infinite_Sum in isabelle-dev
Nov 15 2021
Nov 15 2021
avoid hardwired document output;
user9716869 <user9716869@gmail.com> committed rAFP61e152c118d4: CTR and ETTS: integration with SpecCheck: minor amendments.
CTR and ETTS: integration with SpecCheck: minor amendments
Dominique Unruh <unruh@ut.ee> committed rAFPb3ed7312e4c8: Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL….
Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL…
Dominique Unruh <unruh@ut.ee> committed rAFP4c2a8ccf67f4: Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum.
Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum
Burkhart Wolff <wolff@lri.fr> committed rAFP926aa8675ef8: Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc..
Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc.
Burkhart Wolff <wolff@lri.fr> committed rAFP25c35ef2f771: Added section on C11_Ast_Lib in chapter II..
Added section on C11_Ast_Lib in chapter II.
Burkhart Wolff <wolff@lri.fr> committed rAFP9ee07a7f9824: Example section restored and Documentation adapted..
Example section restored and Documentation adapted.
Burkhart Wolff <wolff@lri.fr> committed rAFP9783556732ec: documentation fine-tuning..
documentation fine-tuning.
Burkhart Wolff <wolff@lri.fr> committed rAFP50eea014c592: Stramge intermediate configuration: Example section zerschossen..
Stramge intermediate configuration: Example section zerschossen.