Page MenuHomeIsabelle/Phabricator
Feed All Stories

Yesterday

desharna committed rISABELLEadb34395b622: added support for unbounded max calls to Mirabelle.
added support for unbounded max calls to Mirabelle
Sat, Jun 12, 3:38 PM
desharna committed rISABELLEbb277f37c34a: added warnings when defining unamed or redefining Mirabelle action.
added warnings when defining unamed or redefining Mirabelle action
Sat, Jun 12, 3:16 PM
makarius committed rISABELLE93228ff7aa67: tuned whitespace;.
tuned whitespace;
Sat, Jun 12, 12:27 PM

Fri, Jun 11

desharna committed rISABELLE4eac16052a94: tuned Mirabelle.
tuned Mirabelle
Fri, Jun 11, 9:38 AM
desharna committed rISABELLE77306bf4e1ee: merged.
merged
Fri, Jun 11, 9:38 AM
desharna committed rISABELLE58f6b41efe88: refactored Mirabelle to produce output in real time.
refactored Mirabelle to produce output in real time
Fri, Jun 11, 9:38 AM

Thu, Jun 10

Asta Halkjær From <andro.from@gmail.com> committed rAFP0730332cf9f6: Fix typo in date.
Fix typo in date
Thu, Jun 10, 4:40 PM
florian.haftmann committed rISABELLEbfce186331be: more succint interfaces.
more succint interfaces
Thu, Jun 10, 9:08 AM
florian.haftmann committed rISABELLE9447668d1b77: global interpretation into nested targets.
global interpretation into nested targets
Thu, Jun 10, 9:08 AM

Wed, Jun 9

makarius created Blog Post: Reactivated ML profiling.
Wed, Jun 9, 12:11 PM
makarius committed rISABELLE8a9fd2ffb81d: merged.
merged
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE014b944f4972: tuned messages;.
tuned messages;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE9134ae401ad5: NEWS;.
NEWS;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE95484bd7e1ec: proper profiling within command execution: messages require PIDE id;.
proper profiling within command execution: messages require PIDE id;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLEa5200fa7cb4c: more systematic treatment of profiling mode;.
more systematic treatment of profiling mode;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE0638fa8c01bc: tuned message;.
tuned message;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE0e6a5a6cc767: prefer less intrusive tracing message;.
prefer less intrusive tracing message;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE690fdc14f7fb: add missing file;.
add missing file;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLEf72335f6a9ed: clarified documentation: tracing messages are not shown here;.
clarified documentation: tracing messages are not shown here;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE5dae03d50db1: more formal ML profiling messages;.
more formal ML profiling messages;
Wed, Jun 9, 11:57 AM
makarius committed rISABELLE364bac6691de: clarified modules;.
clarified modules;
Wed, Jun 9, 11:57 AM

Tue, Jun 8

nipkow committed rAFP337ae29a0d24: Lukas Steven's changes for his fold updates.
Lukas Steven's changes for his fold updates
Tue, Jun 8, 5:06 PM
nipkow committed rISABELLEae2f8144b60d: Lukas Steven's more general fold foctions for maps.
Lukas Steven's more general fold foctions for maps
Tue, Jun 8, 5:02 PM
nipkow committed rISABELLE9db620f007fa: More general fold function for maps.
More general fold function for maps
Tue, Jun 8, 5:01 PM

Mon, Jun 7

makarius committed rISABELLE5153fad491f3: follow Phabricator update 2021 Week 23;.
follow Phabricator update 2021 Week 23;
Mon, Jun 7, 3:14 PM
makarius updated the post content for Blog Post: More predefined Isabelle symbols.
Mon, Jun 7, 2:57 PM
makarius created Blog Post: More predefined Isabelle symbols.
Mon, Jun 7, 2:56 PM
makarius created Blog Post: System options short form (e.g. "-o document").
Mon, Jun 7, 2:45 PM
makarius committed rISABELLE2a431e8bb9b4: tuned;.
tuned;
Mon, Jun 7, 2:41 PM
makarius committed rISABELLEaefa7d210725: more formal theory and session names;.
more formal theory and session names;
Mon, Jun 7, 2:41 PM
makarius committed rISABELLE201200b549fc: proper NEWS after Isabelle2021;.
proper NEWS after Isabelle2021;
Mon, Jun 7, 2:41 PM
makarius committed rISABELLE263dc905d795: updated descriptions;.
updated descriptions;
Mon, Jun 7, 1:05 PM
makarius committed rISABELLE5b49c650d413: tuned;.
tuned;
Mon, Jun 7, 11:48 AM
makarius committed rISABELLE72900f34dbb3: allow system option short form NAME for NAME=true for type string, not just….
allow system option short form NAME for NAME=true for type string, not just…
Mon, Jun 7, 11:48 AM
makarius committed rISABELLE6e9a47d3850c: more robust within session "HOL";.
more robust within session "HOL";
Mon, Jun 7, 11:48 AM

Sun, Jun 6

makarius committed rISABELLEc10fe904ac10: merged.
merged
Sun, Jun 6, 10:01 PM
makarius committed rISABELLE9ead8d9be3ab: clarified hook for Mirabelle: provide all loaded theories at once (for each….
clarified hook for Mirabelle: provide all loaded theories at once (for each…
Sun, Jun 6, 10:01 PM
makarius committed rISABELLE1192c68ebe1c: suppress theories from other sessions, unless explicitly specified via….
suppress theories from other sessions, unless explicitly specified via…
Sun, Jun 6, 10:01 PM
makarius committed rISABELLE745e2cd1f5f5: refer to theory "segments" only, according to global Build.build_theories and….
refer to theory "segments" only, according to global Build.build_theories and…
Sun, Jun 6, 10:01 PM
makarius committed rISABELLE60214976d846: tuned;.
tuned;
Sun, Jun 6, 10:01 PM
makarius committed rISABELLEdf0fd744e6bb: tuned;.
tuned;
Sun, Jun 6, 10:01 PM
makarius committed rISABELLEd67688992bde: more uniform schedule_theories, notably for "present" and "commit" phase after….
more uniform schedule_theories, notably for "present" and "commit" phase after…
Sun, Jun 6, 10:01 PM
florian.haftmann committed rISABELLE0510c7a4256a: moved more legacy to AFP.
moved more legacy to AFP
Sun, Jun 6, 7:01 PM
florian.haftmann committed rAFP0b37c282b057: moved more legacy to AFP.
moved more legacy to AFP
Sun, Jun 6, 7:00 PM
kleing committed rAFP7858c60cc57a: merge from afp-2021.
merge from afp-2021
Sun, Jun 6, 3:17 AM
kleing committed rAFP98a8bdb85f79: merge from afp-2021.
merge from afp-2021
Sun, Jun 6, 3:17 AM
kleing committed rAFP4f1d55756b1a: suppress site-gen warning.
suppress site-gen warning
Sun, Jun 6, 3:17 AM
kleing committed rAFP5fb712317ba8: exclude etc/ in afp_check_roots.
exclude etc/ in afp_check_roots
Sun, Jun 6, 3:17 AM
kleing committed rAFPed3bf7f7bedc: update usage instrucions.
update usage instrucions
Sun, Jun 6, 3:17 AM
kleing committed rAFP52357a42c5e4: strip trailing whitespace; make full URL.
strip trailing whitespace; make full URL
Sun, Jun 6, 3:17 AM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP9f1d39da07c2: sitegen for Lifting_the_Exponent.
sitegen for Lifting_the_Exponent
Sun, Jun 6, 3:17 AM
makarius committed rAFP3a9c2004b599: more robust component setup for AFP/thys: support "isabelle components -u" and….
more robust component setup for AFP/thys: support "isabelle components -u" and…
Sun, Jun 6, 3:17 AM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP804c8ce94283: new entry Lifting_the_Exponent.
new entry Lifting_the_Exponent
Sun, Jun 6, 3:17 AM

Sat, Jun 5

makarius committed rAFP3d11d724cbb4: more specific export_files: omit recent additions ("document", "PIDE", etc.);.
more specific export_files: omit recent additions ("document", "PIDE", etc.);
Sat, Jun 5, 11:43 PM
makarius committed rISABELLE43882e34c038: clarified modules;.
clarified modules;
Sat, Jun 5, 9:10 PM
makarius committed rISABELLEc8b4a4f69068: clarified check (refining fc828f64da5b): etc/settings or etc/components is not….
clarified check (refining fc828f64da5b): etc/settings or etc/components is not…
Sat, Jun 5, 9:10 PM
makarius committed rISABELLE11f611494766: tuned;.
tuned;
Sat, Jun 5, 9:10 PM
makarius committed rISABELLE90b64197bafd: more thorough update of required files (amending 1529c3eb6bac);.
more thorough update of required files (amending 1529c3eb6bac);
Sat, Jun 5, 7:28 PM
makarius committed rISABELLEf143d0a4cb6a: clarified examples;.
clarified examples;
Sat, Jun 5, 2:27 PM
makarius committed rISABELLEce9529a616fd: misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);.
misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);
Sat, Jun 5, 2:27 PM
makarius committed rISABELLE1c5dcba6925f: tuned proofs;.
tuned proofs;
Sat, Jun 5, 2:27 PM
makarius committed rISABELLEda3405e5cd58: tuned --- reduced source complexity;.
tuned --- reduced source complexity;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE6f367240f09b: proper usage (amending f7ea394490f5);.
proper usage (amending f7ea394490f5);
Sat, Jun 5, 12:24 AM
makarius committed rISABELLEb73777a0c076: allow build session setup, e.g. for protocol handlers;.
allow build session setup, e.g. for protocol handlers;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLEb982362eeca4: merged, resolving minor conflict;.
merged, resolving minor conflict;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE451fc6be6c5b: unused;.
unused;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE2141d6c83511: tuned --- potentially more robust (e.g. session.phase_changed vs..
tuned --- potentially more robust (e.g. session.phase_changed vs.
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE8d9ac6cfc270: clarified signature;.
clarified signature;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE4addb9707200: tuned --- avoid redundant future tasks from already loaded theories;.
tuned --- avoid redundant future tasks from already loaded theories;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLEe67c951f1c18: removed pointless option (see 3d0952893db8);.
removed pointless option (see 3d0952893db8);
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE1262fefabc9a: no comment --- topological order appears to be fine since 04-Mar-2013;.
no comment --- topological order appears to be fine since 04-Mar-2013;
Sat, Jun 5, 12:24 AM
makarius committed rISABELLE1ca35197108f: more predictable sequential presentation (2f9877db82a1), without somewhat….
more predictable sequential presentation (2f9877db82a1), without somewhat…
Sat, Jun 5, 12:24 AM

Fri, Jun 4

desharna committed rISABELLEf7ea394490f5: moved stride option from sledgehammer action to main mirabelle.
moved stride option from sledgehammer action to main mirabelle
Fri, Jun 4, 11:12 PM

Thu, Jun 3

paulson committed rISABELLE56f31baaa837: merged.
merged
Thu, Jun 3, 4:02 PM
paulson <lp15@cam.ac.uk> committed rISABELLE8893e0ed263a: new lemmas mostly about paths.
new lemmas mostly about paths
Thu, Jun 3, 4:02 PM
florian.haftmann committed rAFPe2811dc54d05: grouped lemmas.
grouped lemmas
Thu, Jun 3, 8:25 AM
florian.haftmann committed rISABELLEe75635a0bafd: lexorders the locale way.
lexorders the locale way
Thu, Jun 3, 8:05 AM

Wed, Jun 2

florian.haftmann committed rISABELLE26c0ccf17f31: more accurate export morphism enables proper instantiation by interpretation.
more accurate export morphism enables proper instantiation by interpretation
Wed, Jun 2, 5:22 PM

Sun, May 30

florian.haftmann committed rAFPfd98855f4f8e: bundles for traditional infix syntax.
bundles for traditional infix syntax
Sun, May 30, 8:55 AM

Sat, May 29

paulson <lp15@cam.ac.uk> committed rISABELLEe10d530f157a: some new and/or varient results about images.
some new and/or varient results about images
Sat, May 29, 2:52 PM
paulson committed rISABELLEa1086aebcd78: merged.
merged
Sat, May 29, 2:52 PM
paulson <lp15@cam.ac.uk> committed rISABELLE370ce138d1bd: nicer statement of Liouville_theorem.
nicer statement of Liouville_theorem
Sat, May 29, 2:52 PM
florian.haftmann committed rISABELLEaab7975fa070: more lemmas.
more lemmas
Sat, May 29, 7:59 AM
florian.haftmann committed rISABELLE35217bf33215: max word moved to Word_Lib in AFP.
max word moved to Word_Lib in AFP
Sat, May 29, 7:59 AM
florian.haftmann committed rAFPbdcaff25a220: complement reduced to mere abbreviation.
complement reduced to mere abbreviation
Sat, May 29, 7:59 AM
florian.haftmann committed rAFP3ddc21f61385: max word moved to Word_Lib in AFP.
max word moved to Word_Lib in AFP
Sat, May 29, 7:59 AM
florian.haftmann committed rAFPd7c3c888a331: extracted more legacy abbreviations.
extracted more legacy abbreviations
Sat, May 29, 7:59 AM

Fri, May 28

kleing committed rAFPaae69e3e9178: merge from afp-2021.
merge from afp-2021
Fri, May 28, 11:29 AM
kleing committed rAFP33604ec4a9b0: update website.
update website
Fri, May 28, 11:29 AM
kleing committed rAFP19021bb60d89: fix links.
fix links
Fri, May 28, 11:29 AM
lukasstevens committed rAFP84e7b649025b: Restore deleted theorem from Szpilrajn.
Restore deleted theorem from Szpilrajn
Fri, May 28, 10:49 AM

Thu, May 27

florian.haftmann committed rAFP7c0105d2d63f: tuned presentation.
tuned presentation
Thu, May 27, 11:31 PM
kleing committed rAFP6605c2eb8bc8: merge from afp-2021.
merge from afp-2021
Thu, May 27, 11:31 PM
nipkow committed rAFP83f656769137: adapted to devel.
adapted to devel
Thu, May 27, 11:31 PM
florian.haftmann committed rAFPd92f99905ee2: adjusted to changes in distribution.
adjusted to changes in distribution
Thu, May 27, 11:31 PM
kleing committed rAFP6d986a7dc22b: make AFP ROOTS globally available for component.
make AFP ROOTS globally available for component
Thu, May 27, 11:31 PM
nipkow committed rAFP772899cc7640: merged.
merged
Thu, May 27, 11:31 PM
kleing committed rAFP55f94db4dfd0: adjust Combinatorics_Words to isabelle@493b1ae188da.
adjust Combinatorics_Words to isabelle@493b1ae188da
Thu, May 27, 11:31 PM
nipkow committed rAFPee3c49419315: New entries Combinatorics_Words*.
New entries Combinatorics_Words*
Thu, May 27, 11:31 PM
florian.haftmann committed rAFP97869e45578a: adjusted to change in distribution.
adjusted to change in distribution
Thu, May 27, 11:31 PM