Page MenuHomeIsabelle/Phabricator
Feed All Stories

Nov 26 2021

makarius committed rISABELLE8d7d082c1649: clarified modules (see c299abcf7081);.
clarified modules (see c299abcf7081);
Nov 26 2021, 9:08 PM
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…
Nov 26 2021, 9:08 PM
makarius committed rISABELLEc299abcf7081: clarified modules;.
clarified modules;
Nov 26 2021, 9:08 PM
makarius committed rISABELLE32490add64b4: tuned signature: more explicit types for presentation;.
tuned signature: more explicit types for presentation;
Nov 26 2021, 9:08 PM
makarius committed rISABELLE40bb5f41e06c: more robust support for Windows line-endings;.
more robust support for Windows line-endings;
Nov 26 2021, 9:07 PM
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…
Nov 26 2021, 9:07 PM
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…
Nov 26 2021, 9:07 PM
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…
Nov 26 2021, 9:07 PM
makarius committed rISABELLE0e4d8aa61ad7: more symbolic latex_output via XML (using YXML within text);.
more symbolic latex_output via XML (using YXML within text);
Nov 26 2021, 9:07 PM
makarius committed rISABELLE9bea6244c35a: proper enclose_name (amending e77c5bfca9aa);.
proper enclose_name (amending e77c5bfca9aa);
Nov 26 2021, 9:07 PM
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.
Nov 26 2021, 9:07 PM
makarius committed rISABELLE5f73bc0b9e5e: tuned;.
tuned;
Nov 26 2021, 9:07 PM
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…
Nov 26 2021, 9:07 PM
makarius committed rISABELLEd6ce4ce20422: more symbolic latex_output via XML;.
more symbolic latex_output via XML;
Nov 26 2021, 9:07 PM
makarius committed rISABELLEed3adabf0dbe: updated to verit-2021.06.2-rmx;.
updated to verit-2021.06.2-rmx;
Nov 26 2021, 9:07 PM
makarius committed rISABELLE98b3c7ab8c0f: tuned;.
tuned;
Nov 26 2021, 9:07 PM
makarius committed rISABELLE3064e165c660: clarified HTML_Context.theory_exports: prefer value-oriented parallelism;.
clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
Nov 26 2021, 9:07 PM
makarius committed rISABELLEcfc15da73a78: afford more parallelism for sessions (instead of theories in 5eac4b13d1f1)….
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1)…
Nov 26 2021, 9:07 PM
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;
Nov 26 2021, 9:07 PM
mathias.fleury committed rISABELLE1fd8705503b4: generate problems with correct logic for veriT.
generate problems with correct logic for veriT
Nov 26 2021, 9:07 PM
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…
Nov 26 2021, 9:07 PM
makarius committed rISABELLE79fa9f2d02fa: more interrupts;.
more interrupts;
Nov 26 2021, 9:07 PM
makarius committed rISABELLE4543fb2b5ef2: tuned;.
tuned;
Nov 26 2021, 9:07 PM
makarius committed rISABELLE1f40ded31b78: clarified modules;.
clarified modules;
Nov 26 2021, 9:07 PM
makarius committed rISABELLEd540c36cd0d2: tuned (see also e0d1d9203275);.
tuned (see also e0d1d9203275);
Nov 26 2021, 9:07 PM
makarius committed rISABELLE23dc565cd4b2: tuned;.
tuned;
Nov 26 2021, 9:07 PM
makarius committed rISABELLE48fda7ee1973: clarified signature;.
clarified signature;
Nov 26 2021, 9:07 PM
makarius committed rISABELLEd1d3d4439ac2: spelling;.
spelling;
Nov 26 2021, 9:07 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2021-1.
Nov 26 2021, 9:04 PM
desharna committed rISABELLEb65336541c19: renamed multp_code_iff and multeqp_code_iff.
renamed multp_code_iff and multeqp_code_iff
Nov 26 2021, 4:33 PM
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
Nov 26 2021, 4:33 PM
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.
Nov 26 2021, 9:16 AM
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 26 2021, 9:01 AM

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;
Nov 25 2021, 4:13 PM
desharna committed rISABELLE825cd198d85c: renamed Multiset.multp and Multiset.multeqp.
renamed Multiset.multp and Multiset.multeqp
Nov 25 2021, 4:10 PM
Fabian Huch <huch@in.tum.de> committed rAFPcea71b734a23: added keywords to site generated entry data;.
added keywords to site generated entry data;
Nov 25 2021, 3:31 PM
Fabian Huch <huch@in.tum.de> committed rAFPa53823fdccd8: improved keyword extraction;.
improved keyword extraction;
Nov 25 2021, 3:31 PM
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;
Nov 25 2021, 3:31 PM
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 25 2021, 3:31 PM

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 23 2021, 8:20 PM

Nov 22 2021

Fabian Huch <huch@in.tum.de> committed rAFP5857c4582eae: integrated metadata changes into site;.
integrated metadata changes into site;
Nov 22 2021, 6:58 PM
Fabian Huch <huch@in.tum.de> committed rAFP09790a81f454: added missing keyword data;.
added missing keyword data;
Nov 22 2021, 6:33 PM
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);
Nov 22 2021, 5:44 PM
Fabian Huch <huch@in.tum.de> committed rAFPc5355362ec54: tuned sitegen: moved dependencies generation to scala.
tuned sitegen: moved dependencies generation to scala
Nov 22 2021, 5:44 PM
Fabian Huch <huch@in.tum.de> committed rAFPdf920a57d3cf: changed generated author format;.
changed generated author format;
Nov 22 2021, 5:44 PM
Fabian Huch <huch@in.tum.de> committed rAFPf09cb003fe3c: tuned;.
tuned;
Nov 22 2021, 5:44 PM
Fabian Huch <huch@in.tum.de> committed rAFP2b9064e3aaa4: tuned hugo: static files more explicit;.
tuned hugo: static files more explicit;
Nov 22 2021, 5:44 PM
Fabian Huch <huch@in.tum.de> committed rAFPf69e70cf8a17: tuned;.
tuned;
Nov 22 2021, 5:44 PM

Nov 17 2021

nipkow committed rISABELLEb61bd2c12de3: added lemmas.
added lemmas
Nov 17 2021, 10:26 PM
paulson <lp15@cam.ac.uk> committed rAFP1fe98b11c666: A slightly stronger lemma allowing slightly simpler proofs.
A slightly stronger lemma allowing slightly simpler proofs
Nov 17 2021, 5:01 PM
Fabian Huch <huch@in.tum.de> committed rAFP12628bcb34d2: tuned;.
tuned;
Nov 17 2021, 9:23 AM
Fabian Huch <huch@in.tum.de> committed rAFPd7cd94262b1a: added missing name mapping to migration;.
added missing name mapping to migration;
Nov 17 2021, 9:23 AM
Fabian Huch <huch@in.tum.de> committed rAFPf81257bb1f6d: clarified hugo data;.
clarified hugo data;
Nov 17 2021, 9:23 AM
Fabian Huch <huch@in.tum.de> committed rAFP29324715b4d0: proper authors/affiliations gen for hugo taxonomy;.
proper authors/affiliations gen for hugo taxonomy;
Nov 17 2021, 9:23 AM
Fabian Huch <huch@in.tum.de> committed rAFPa125cf87f609: proper output path;.
proper output path;
Nov 17 2021, 9:23 AM

Nov 16 2021

makarius committed rISABELLE189248f76ed8: merged.
merged
Nov 16 2021, 9:57 PM
makarius committed rISABELLE3dfb8e47a6b7: removed redundant test (see also 86fac52c2795, a9fea3f11cc0);.
removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
Nov 16 2021, 9:57 PM
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…
Nov 16 2021, 9:57 PM
makarius committed rISABELLE9bf6b5ed9af4: tuned;.
tuned;
Nov 16 2021, 9:57 PM
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…
Nov 16 2021, 9:57 PM
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…
Nov 16 2021, 9:57 PM
makarius committed rISABELLE1c2863734db1: proper version;.
proper version;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEb6f6e3ca2bdc: updated NEWS: arm64-linux support is almost complete;.
updated NEWS: arm64-linux support is almost complete;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEc606fddc5b05: slightly faster XML output: avoid too much regrowing of StringBuilder;.
slightly faster XML output: avoid too much regrowing of StringBuilder;
Nov 16 2021, 9:57 PM
pruvisto committed rISABELLE227915e07891: more material for HOL-Analysis.Infinite_Sum.
more material for HOL-Analysis.Infinite_Sum
Nov 16 2021, 9:57 PM
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…
Nov 16 2021, 9:57 PM
makarius committed rISABELLE3ce6fb9db485: more symbolic latex_output via XML;.
more symbolic latex_output via XML;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE95e514137861: updated to polyml-5.9-610a153b941d -- close to final;.
updated to polyml-5.9-610a153b941d -- close to final;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEa5c23da73fca: clarified signature;.
clarified signature;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE543f932f64b8: more symbolic latex output;.
more symbolic latex output;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE4671d29feb00: tuned signature;.
tuned signature;
Nov 16 2021, 9:57 PM
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;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEd2522bb4db1b: symbolic latex_output via XML, interpreted in Isabelle/Scala;.
symbolic latex_output via XML, interpreted in Isabelle/Scala;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE47f565849e71: tuned signature;.
tuned signature;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE0a87ea7eb76f: clarified signature;.
clarified signature;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEffd640825505: clarified signature;.
clarified signature;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE5fca489a6ac1: tuned output --- less redundancy;.
tuned output --- less redundancy;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE6504e9b09926: clarified signature: more privacy;.
clarified signature: more privacy;
Nov 16 2021, 9:57 PM
makarius committed rISABELLEa1a316442a9b: tuned whitespace;.
tuned whitespace;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE2fd0c33fe440: clarified signature: Latex.Output as parameter to Document_Build.Engine;.
clarified signature: Latex.Output as parameter to Document_Build.Engine;
Nov 16 2021, 9:57 PM
makarius committed rISABELLE251bf0f2d5bb: proper detection of ARM platform variants;.
proper detection of ARM platform variants;
Nov 16 2021, 9:57 PM
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…
Nov 16 2021, 3:37 PM
paulson <lp15@cam.ac.uk> committed rAFP619663adf685: Elimination of all z3 calls.
Elimination of all z3 calls
Nov 16 2021, 3:13 PM
kleing committed rAFP7a2522dce834: Word_Lib sync from l4v; tweak word_eqI.
Word_Lib sync from l4v; tweak word_eqI
Nov 16 2021, 7:12 AM
kleing committed rAFP4735e2db8e29: generalise word_eqI method; make sure it is exercised.
generalise word_eqI method; make sure it is exercised
Nov 16 2021, 5:44 AM
kleing committed rAFP145a2429825e: test_bit_size not longer needed; avoid potential nontermination.
test_bit_size not longer needed; avoid potential nontermination
Nov 16 2021, 1:51 AM
kleing committed rAFP4723cbfda63e: Word_Lib tweaks for slightly more backwards compatibility.
Word_Lib tweaks for slightly more backwards compatibility
Nov 16 2021, 12:52 AM
kleing committed rAFP5d1795962da2: use bit_simps in word_eqI method.
use bit_simps in word_eqI method
Nov 16 2021, 12:52 AM
pruvisto committed rAFP7aec7688b019: adapted to new version of Infinite_Sum in isabelle-dev.
adapted to new version of Infinite_Sum in isabelle-dev
Nov 16 2021, 12:00 AM

Nov 15 2021

makarius committed rAFP22694dc0d736: avoid hardwired document output;.
avoid hardwired document output;
Nov 15 2021, 11:23 PM
user9716869 <user9716869@gmail.com> committed rAFP61e152c118d4: CTR and ETTS: integration with SpecCheck: minor amendments.
CTR and ETTS: integration with SpecCheck: minor amendments
Nov 15 2021, 8:07 PM
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…
Nov 15 2021, 6:16 PM
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
Nov 15 2021, 3:46 PM
Burkhart Wolff <wolff@lri.fr> committed rAFP279f0ad553e8: merge.
merge
Nov 15 2021, 2:49 PM
Burkhart Wolff <wolff@lri.fr> committed rAFPe3de3e8bc7e6: merge.
merge
Nov 15 2021, 2:49 PM
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.
Nov 15 2021, 2:49 PM
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.
Nov 15 2021, 2:48 PM
Burkhart Wolff <wolff@lri.fr> committed rAFP9ee07a7f9824: Example section restored and Documentation adapted..
Example section restored and Documentation adapted.
Nov 15 2021, 2:48 PM
Burkhart Wolff <wolff@lri.fr> committed rAFP9783556732ec: documentation fine-tuning..
documentation fine-tuning.
Nov 15 2021, 2:48 PM
Burkhart Wolff <wolff@lri.fr> committed rAFP50eea014c592: Stramge intermediate configuration: Example section zerschossen..
Stramge intermediate configuration: Example section zerschossen.
Nov 15 2021, 2:48 PM