| Author | Object | Transaction | Date |
|---|
| kleing | rAFP7858c60cc57a: merge from afp-2021 | | Jun 6 2021, 3:06 AM |
| kleing | rAFP4f1d55756b1a: suppress site-gen warning | | Jun 6 2021, 3:05 AM |
| kleing | rAFPed3bf7f7bedc: update usage instrucions | | Jun 6 2021, 2:48 AM |
| kleing | rAFP5fb712317ba8: exclude etc/ in afp_check_roots | | Jun 6 2021, 2:47 AM |
| kleing | rAFP52357a42c5e4: strip trailing whitespace; make full URL | | Jun 6 2021, 2:46 AM |
| makarius | rAFP3d11d724cbb4: more specific export_files: omit recent additions ("document", "PIDE", etc.); | | Jun 5 2021, 11:32 PM |
| makarius | rISABELLEc8b4a4f69068: clarified check (refining fc828f64da5b): etc/settings or etc/components is not… | | Jun 5 2021, 9:10 PM |
| makarius | rISABELLEfc828f64da5b: support isabelle components -u and -x; | | Jun 5 2021, 9:10 PM |
| makarius | rISABELLE43882e34c038: clarified modules; | | Jun 5 2021, 9:01 PM |
| makarius | rAFP3a9c2004b599: more robust component setup for AFP/thys: support "isabelle components -u" and… | | Jun 5 2021, 8:44 PM |
| makarius | rISABELLEc8b4a4f69068: clarified check (refining fc828f64da5b): etc/settings or etc/components is not… | | Jun 5 2021, 8:20 PM |
| makarius | rISABELLE11f611494766: tuned; | | Jun 5 2021, 8:15 PM |
| makarius | rISABELLE90b64197bafd: more thorough update of required files (amending 1529c3eb6bac); | | Jun 5 2021, 7:28 PM |
| makarius | rISABELLE1529c3eb6bac: more thorough update of options; | | Jun 5 2021, 7:28 PM |
| makarius | rISABELLE90b64197bafd: more thorough update of required files (amending 1529c3eb6bac); | | Jun 5 2021, 7:21 PM |
| makarius | rISABELLE1ce1bc9ff64a: added old chestnut | | Jun 5 2021, 2:27 PM |
| makarius | rISABELLEce9529a616fd: misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); | | Jun 5 2021, 2:27 PM |
| makarius | URI 10 https://isabelle.in.tum.de/repos/isabelle | makarius changed the display type for this URI from "No I/O" to "Observe". | Jun 5 2021, 2:27 PM |
| makarius | URI 41 ssh://i21isatest@isabelle.in.tum.de//p/home/isabelle-repository/repos/isabelle | makarius changed the display type for this URI from "Observe" to "No I/O". | Jun 5 2021, 2:26 PM |
| makarius | rISABELLEf143d0a4cb6a: clarified examples; | | Jun 5 2021, 12:57 PM |
| makarius | rISABELLE1c5dcba6925f: tuned proofs; | | Jun 5 2021, 12:45 PM |
| makarius | rISABELLEce9529a616fd: misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); | | Jun 5 2021, 12:29 PM |
| makarius | rISABELLEf7ea394490f5: moved stride option from sledgehammer action to main mirabelle | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLE6f367240f09b: proper usage (amending f7ea394490f5); | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLE3d0952893db8: proper build of required session images vs. build with Mirabelle presentation; | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLEe67c951f1c18: removed pointless option (see 3d0952893db8); | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLEe7fab0b5dbe7: join all proofs before scheduling present phase (ordered according to weight); | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLE1ca35197108f: more predictable sequential presentation (2f9877db82a1), without somewhat… | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLE2f9877db82a1: reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool… | | Jun 5 2021, 12:24 AM |
| makarius | rISABELLEda3405e5cd58: tuned --- reduced source complexity; | | Jun 4 2021, 11:55 PM |
| makarius | rISABELLE6f367240f09b: proper usage (amending f7ea394490f5); | | Jun 4 2021, 11:40 PM |
| makarius | rISABELLEb982362eeca4: merged, resolving minor conflict; | | Jun 4 2021, 11:37 PM |
| makarius | rISABELLEb73777a0c076: allow build session setup, e.g. for protocol handlers; | | Jun 4 2021, 11:30 PM |
| desharna | rISABELLEf7ea394490f5: moved stride option from sledgehammer action to main mirabelle | | Jun 4 2021, 11:03 PM |
| makarius | rISABELLE451fc6be6c5b: unused; | | Jun 4 2021, 10:58 PM |
| makarius | rISABELLE2141d6c83511: tuned --- potentially more robust (e.g. session.phase_changed vs. | | Jun 4 2021, 10:50 PM |
| makarius | rISABELLE8d9ac6cfc270: clarified signature; | | Jun 4 2021, 10:46 PM |
| makarius | rISABELLEe67c951f1c18: removed pointless option (see 3d0952893db8); | | Jun 4 2021, 10:30 PM |
| makarius | rISABELLE4addb9707200: tuned --- avoid redundant future tasks from already loaded theories; | | Jun 4 2021, 10:01 PM |
| makarius | rISABELLE1262fefabc9a: no comment --- topological order appears to be fine since 04-Mar-2013; | | Jun 4 2021, 9:46 PM |
| makarius | rISABELLE1ca35197108f: more predictable sequential presentation (2f9877db82a1), without somewhat… | | Jun 4 2021, 9:36 PM |
| paulson | rISABELLE56f31baaa837: merged | | Jun 3 2021, 11:58 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE8893e0ed263a: new lemmas mostly about paths | | Jun 3 2021, 11:47 AM |
| florian.haftmann | rAFPe2811dc54d05: grouped lemmas | | Jun 2 2021, 2:46 PM |
| florian.haftmann | rISABELLEe75635a0bafd: lexorders the locale way | | Jun 2 2021, 2:45 PM |
| nipkow | rISABELLE9db620f007fa: More general fold function for maps | | Jun 1 2021, 7:46 PM |
| florian.haftmann | rISABELLE26c0ccf17f31: more accurate export morphism enables proper instantiation by interpretation | | May 31 2021, 10:27 PM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP9f1d39da07c2: sitegen for Lifting_the_Exponent | | May 31 2021, 8:30 PM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP804c8ce94283: new entry Lifting_the_Exponent | | May 31 2021, 8:27 PM |
| florian.haftmann | rAFPfd98855f4f8e: bundles for traditional infix syntax | | May 29 2021, 9:27 PM |
| paulson | rISABELLEa1086aebcd78: merged | | May 29 2021, 2:42 PM |
| florian.haftmann | rAFPbdcaff25a220: complement reduced to mere abbreviation | | May 28 2021, 10:21 PM |
| florian.haftmann | rAFPd7c3c888a331: extracted more legacy abbreviations | | May 28 2021, 10:21 PM |
| florian.haftmann | rISABELLEaab7975fa070: more lemmas | | May 28 2021, 10:21 PM |
| florian.haftmann | rAFP3ddc21f61385: max word moved to Word_Lib in AFP | | May 28 2021, 10:21 PM |
| florian.haftmann | rISABELLE35217bf33215: max word moved to Word_Lib in AFP | | May 28 2021, 10:21 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEe10d530f157a: some new and/or varient results about images | | May 28 2021, 7:11 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE370ce138d1bd: nicer statement of Liouville_theorem | | May 28 2021, 3:43 PM |
| kleing | rAFPaae69e3e9178: merge from afp-2021 | | May 28 2021, 11:29 AM |
| kleing | rAFP33604ec4a9b0: update website | | May 28 2021, 11:24 AM |
| lukasstevens | rAFP84e7b649025b: Restore deleted theorem from Szpilrajn | | May 28 2021, 10:47 AM |
| kleing | rAFP19021bb60d89: fix links | | May 28 2021, 7:07 AM |
| makarius | rISABELLE466fae6bf22e: compose Latex text as XML, output exported YXML in Isabelle/Scala; | | May 27 2021, 11:31 PM |
| makarius | rAFPd198fb4d73bd: adapted to Isabelle/466fae6bf22e; | | May 27 2021, 11:31 PM |
| makarius | rAFP2c2eaa6a32e2: adapted to Isabelle/ef1a18e20ace; | | May 27 2021, 11:31 PM |
| makarius | rISABELLEef1a18e20ace: clarified modules; | | May 27 2021, 11:31 PM |
| florian.haftmann | rAFP7c0105d2d63f: tuned presentation | | May 27 2021, 3:06 PM |
| nipkow | rAFP83f656769137: adapted to devel | | May 27 2021, 11:38 AM |
| florian.haftmann | rAFPd92f99905ee2: adjusted to changes in distribution | | May 27 2021, 9:12 AM |
| kleing | rAFP55f94db4dfd0: adjust Combinatorics_Words to isabelle@493b1ae188da | | May 27 2021, 2:58 AM |
| kleing | rAFP6605c2eb8bc8: merge from afp-2021 | | May 27 2021, 2:09 AM |
| kleing | rAFP6d986a7dc22b: make AFP ROOTS globally available for component | | May 27 2021, 2:07 AM |
| makarius | rISABELLE493b1ae188da: more robust syntax; | | May 26 2021, 6:07 PM |
| florian.haftmann | rAFP97869e45578a: adjusted to change in distribution | | May 26 2021, 5:26 PM |
| makarius | rISABELLE0909fd14f8a4: avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; | | May 26 2021, 2:19 PM |
| makarius | rISABELLE52030acb19ac: option document_build refers to build engine in Isabelle/Scala; | | May 26 2021, 2:19 PM |
| nipkow | rAFP772899cc7640: merged | | May 26 2021, 12:05 PM |
| nipkow | rAFPee3c49419315: New entries Combinatorics_Words* | | May 26 2021, 11:59 AM |
| makarius | rISABELLE18d80cd51823: unused; | | May 25 2021, 11:58 PM |
| makarius | rISABELLEb5fb99b985b4: clarified document export names; | | May 25 2021, 11:37 PM |
| makarius | rISABELLE04d39959d1e6: tuned signature; | | May 25 2021, 11:18 PM |
| makarius | rISABELLEe4d50a660140: tuned; | | May 25 2021, 11:12 PM |
| makarius | rISABELLE4606a9cadd83: tuned; | | May 25 2021, 11:04 PM |
| makarius | rISABELLE0909fd14f8a4: avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; | | May 25 2021, 11:00 PM |
| makarius | rAFPd198fb4d73bd: adapted to Isabelle/466fae6bf22e; | | May 25 2021, 10:35 PM |
| makarius | rISABELLE466fae6bf22e: compose Latex text as XML, output exported YXML in Isabelle/Scala; | | May 25 2021, 10:28 PM |
| makarius | rAFP551b996da2ca: tuned whitespace; | | May 25 2021, 10:14 PM |
| makarius | rISABELLE546e1e591635: more direct index_entry: no positions required -- text is eventually moved to . | | May 25 2021, 9:44 PM |
| makarius | rISABELLEa383c4340c25: clarified signature; | | May 25 2021, 9:32 PM |
| n.muendler <n.muendler@tum.de> | rAFPe85ad91917fa: Remove comment about missing refinement | | May 25 2021, 1:35 PM |
| paulson <lp15@cam.ac.uk> | rAFP96fa84024913: continued uglification, but also fixed some dodgy proofs | | May 25 2021, 12:40 PM |
| dcjm | rPOLYML00a5653c7373: The file part of the command for Unix.execute/executeInEnv should be included… | | May 25 2021, 12:01 PM |
| dcjm | rPOLYML2b78b6865011: Enable all signals in child process after Unix.execute/executeInEnv. | | May 25 2021, 12:01 PM |
| dcjm | rPOLYML8185978a586a: Enable all signals in child process after Unix.execute/executeInEnv. | | May 24 2021, 8:29 PM |
| paulson <lp15@cam.ac.uk> | rAFP0c01ef559f08: fixed some broken / looping / fragile proofs | | May 24 2021, 4:45 PM |
| makarius | rISABELLEb50f8cc8c08e: support for base64 via Isabelle/Scala/ML; | | May 24 2021, 1:23 PM |
| makarius | rISABELLE6bd747b71bd3: proper signature export (amending b50f8cc8c08e); | | May 24 2021, 1:23 PM |
| makarius | rISABELLE52e43a93d51f: clarified system_log: make this work independently of the particular "isabelle… | | May 24 2021, 11:58 AM |
| kleing | rAFP17e46e9fdfda: merge from afp-2021 | | May 24 2021, 2:23 AM |
| kleing | rAFP0c83e74a221f: simplify usage instructions more | | May 24 2021, 2:11 AM |