Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
florian.haftmannrISABELLEd156b141fe2f: mergedJun 23 2021, 8:38 PM
florian.haftmannrAFPf1195cc96e85: more default simp rulesJun 23 2021, 7:43 PM
florian.haftmannrAFP9e42e0c5f9f9: some word streamliningJun 23 2021, 7:43 PM
florian.haftmannrISABELLE7181130f5872: more default simp rulesJun 23 2021, 7:43 PM
florian.haftmannrISABELLE465846b611d5: some word streamliningJun 23 2021, 7:43 PM
makariusrISABELLE3d3c60a90af5: avoid legacy domain informatik.tu-muenchen.de;Jun 23 2021, 5:39 PM
paulson <lp15@cam.ac.uk>rAFP2241611aef17: fixed a messy reference
paulson <lp15@cam.ac.uk> committed rAFP2241611aef17: fixed a messy reference. 
Jun 23 2021, 12:33 PM
paulson <lp15@cam.ac.uk>rAFP1f48f33779db: Van_der_Waerden website
paulson <lp15@cam.ac.uk> committed rAFP1f48f33779db: Van_der_Waerden website. 
Jun 23 2021, 12:17 PM
paulson <lp15@cam.ac.uk>rAFPa3c7e21a602f: new entry Van_der_Waerden
paulson <lp15@cam.ac.uk> committed rAFPa3c7e21a602f: new entry Van_der_Waerden. 
Jun 23 2021, 12:12 PM
florian.haftmannrAFP55af834ad1b8: made consistent againJun 22 2021, 4:02 PM
Fabian Huch <huch@in.tum.de>rAFP291a8d8961b4: Fixed entry name for theories in sub-directoryJun 21 2021, 4:57 PM
nipkowrAFP6424fbf12644: New entry IMP_CompilerJun 21 2021, 9:04 AM
Walter Guttmann <walter.guttmann@canterbury.ac.nz>rAFPd6c66721438d: Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata
Walter Guttmann <walter.guttmann@canterbury.ac.nz> committed rAFPd6c66721438d: Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata. 
Jun 20 2021, 2:09 AM
Walter Guttmann <walter.guttmann@canterbury.ac.nz>rAFP7b56a9ce5619: Relational_Disjoint_Set_Forests: updated metadata to reflect added theory
Walter Guttmann <walter.guttmann@canterbury.ac.nz> committed rAFP7b56a9ce5619: Relational_Disjoint_Set_Forests: updated metadata to reflect added theory. 
Jun 19 2021, 7:56 AM
Walter Guttmann <walter.guttmann@canterbury.ac.nz>rAFP98c7aa03457d: Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests
Walter Guttmann <walter.guttmann@canterbury.ac.nz> committed rAFP98c7aa03457d: Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests. 
Jun 19 2021, 6:59 AM
makariusrISABELLE66bff50bc5f1: tuned --- following hints by IntelliJ;Jun 18 2021, 3:03 PM
makariusrISABELLE4e94ceabaaad: tuned signature;Jun 18 2021, 2:35 PM
makariusrISABELLEdfac078e5444: tuned signature (see 2d6a489adb01);Jun 18 2021, 2:25 PM
makariusrISABELLE2d6a489adb01: clarified signature;Jun 18 2021, 2:25 PM
makariusrISABELLEac5a72740f3a: tuned;Jun 18 2021, 12:13 PM
makariusrISABELLE9594d8e33c57: tuned;Jun 18 2021, 12:13 PM
makariusrISABELLE38fe15a42ff2: tuned signature;Jun 18 2021, 12:12 PM
makariusrISABELLEaa0b1fbe6be3: tuned;Jun 18 2021, 11:48 AM
makariusrISABELLEdfac078e5444: tuned signature (see 2d6a489adb01);Jun 18 2021, 11:32 AM
desharnarISABELLEbc263f1f68cd: added support for TFX's and THF's $ite to SledgehammerJun 17 2021, 12:57 PM
desharnarISABELLE4538d6ffafbd: tuned Mirabelle documentationJun 17 2021, 11:27 AM
desharnarISABELLEa88427e55371: shortened long linesJun 17 2021, 10:46 AM
desharnarISABELLE07675be65227: fixed typosJun 17 2021, 10:43 AM
desharnarISABELLEc55980cf7374: updated Mirabelle documentationJun 17 2021, 10:37 AM
desharnarISABELLEeab5cd9c7862: changed Mirabelle's filter to use short theory namesJun 17 2021, 10:30 AM
florian.haftmannrAFP06eb6c7d6c76: lemma groomingJun 17 2021, 8:18 AM
florian.haftmannrAFPc2595f7c289f: no duplicates of shift operationsJun 16 2021, 10:19 AM
florian.haftmannrISABELLE52b829b18066: more lemmasJun 16 2021, 10:19 AM
kleingrAFP2e179108e08f: merge Jinja/Isar workJun 15 2021, 2:56 AM
desharnarAFP5e24878a9118: updated change history for Interpreter_OptimizationJun 14 2021, 3:04 PM
paulsonrAFP29da90822fc7: merged
paulson committed rAFP29da90822fc7: merged. 
Jun 14 2021, 1:59 PM
paulson <lp15@cam.ac.uk>rAFPa51be9ca4b87: updated, replacing axiomatizations by proper localesJun 14 2021, 1:59 PM
desharnarAFP95f457f69761: added basic blocksJun 14 2021, 10:53 AM
desharnarISABELLEadb34395b622: added support for unbounded max calls to MirabelleJun 12 2021, 3:37 PM
desharnarISABELLEbb277f37c34a: added warnings when defining unamed or redefining Mirabelle actionJun 12 2021, 12:39 PM
makariusrISABELLE93228ff7aa67: tuned whitespace;Jun 12 2021, 12:16 PM
desharnarISABELLE4eac16052a94: tuned MirabelleJun 11 2021, 9:33 AM
Asta Halkjær From <andro.from@gmail.com>rAFP0730332cf9f6: Fix typo in date
Asta Halkjær From <andro.from@gmail.com> committed rAFP0730332cf9f6: Fix typo in date. 
Jun 10 2021, 4:36 PM
desharnarISABELLE77306bf4e1ee: merged
desharna committed rISABELLE77306bf4e1ee: merged. 
Jun 10 2021, 11:54 AM
desharnarISABELLE58f6b41efe88: refactored Mirabelle to produce output in real timeJun 10 2021, 11:21 AM
florian.haftmannrISABELLE9447668d1b77: global interpretation into nested targetsJun 9 2021, 8:04 PM
florian.haftmannrISABELLEbfce186331be: more succint interfacesJun 9 2021, 8:04 PM
makariusrISABELLE014b944f4972: tuned messages;Jun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profiling
makarius set this post's subtitle to "". 
Jun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profiling
makarius created this post. 
Jun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profiling
makarius updated the post content. 
Jun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profiling
makarius renamed this blog post from to Reactivated ML profiling. 
Jun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profilingJun 9 2021, 12:11 PM
makariusBlog Post: Reactivated ML profiling
makarius published this post. 
Jun 9 2021, 12:11 PM
makariusrISABELLE8a9fd2ffb81d: mergedJun 9 2021, 11:25 AM
makariusrISABELLE014b944f4972: tuned messages;Jun 9 2021, 11:21 AM
makariusrISABELLE9134ae401ad5: NEWS;Jun 9 2021, 10:58 AM
makariusrISABELLE95484bd7e1ec: proper profiling within command execution: messages require PIDE id;Jun 9 2021, 10:52 AM
makariusrISABELLEa5200fa7cb4c: more systematic treatment of profiling mode;Jun 9 2021, 10:37 AM
makariusrISABELLE0638fa8c01bc: tuned message;Jun 8 2021, 11:36 PM
makariusrISABELLE0e6a5a6cc767: prefer less intrusive tracing message;Jun 8 2021, 11:34 PM
makariusrISABELLEf72335f6a9ed: clarified documentation: tracing messages are not shown here;Jun 8 2021, 11:23 PM
nipkowrISABELLEae2f8144b60d: Lukas Steven's more general fold foctions for mapsJun 8 2021, 5:01 PM
nipkowrAFP337ae29a0d24: Lukas Steven's changes for his fold updatesJun 8 2021, 4:59 PM
makariusrISABELLE690fdc14f7fb: add missing file;Jun 8 2021, 4:32 PM
makariusrISABELLE5dae03d50db1: more formal ML profiling messages;Jun 8 2021, 1:17 PM
makariusrISABELLE364bac6691de: clarified modules;Jun 7 2021, 4:40 PM
makariusrISABELLE5153fad491f3: follow Phabricator update 2021 Week 23;Jun 7 2021, 3:13 PM
makariusrISABELLE2a431e8bb9b4: tuned;Jun 7 2021, 2:57 PM
makariusBlog Post: More predefined Isabelle symbolsJun 7 2021, 2:57 PM
makariusBlog Post: More predefined Isabelle symbols
makarius updated the post content. 
Jun 7 2021, 2:57 PM
makariusBlog Post: More predefined Isabelle symbols
makarius created this post. 
Jun 7 2021, 2:56 PM
makariusBlog Post: More predefined Isabelle symbols
makarius renamed this blog post from to More predefined Isabelle symbols. 
Jun 7 2021, 2:56 PM
makariusBlog Post: More predefined Isabelle symbols
makarius updated the post content. 
Jun 7 2021, 2:56 PM
makariusBlog Post: More predefined Isabelle symbols
makarius published this post. 
Jun 7 2021, 2:56 PM
makariusBlog Post: More predefined Isabelle symbols
makarius set this post's subtitle to "". 
Jun 7 2021, 2:56 PM
makariusrISABELLE2a431e8bb9b4: tuned;Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")
makarius renamed this blog post from to System options short form (e.g. "-o document"). 
Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")
makarius created this post. 
Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")
makarius set this post's subtitle to "". 
Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")
makarius updated the post content. 
Jun 7 2021, 2:45 PM
makariusBlog Post: System options short form (e.g. "-o document")
makarius published this post. 
Jun 7 2021, 2:45 PM
makariusrISABELLE2a431e8bb9b4: tuned;Jun 7 2021, 2:41 PM
makariusrISABELLEaefa7d210725: more formal theory and session names;Jun 7 2021, 2:40 PM
makariusrISABELLE201200b549fc: proper NEWS after Isabelle2021;Jun 7 2021, 2:34 PM
makariusrISABELLE263dc905d795: updated descriptions;Jun 7 2021, 1:04 PM
makariusrISABELLE72900f34dbb3: allow system option short form NAME for NAME=true for type string, not just…Jun 7 2021, 11:42 AM
makariusrISABELLE5b49c650d413: tuned;Jun 7 2021, 9:36 AM
makariusrISABELLE6e9a47d3850c: more robust within session "HOL";Jun 7 2021, 9:27 AM
makariusrISABELLEc10fe904ac10: mergedJun 6 2021, 9:39 PM
makariusrISABELLE1192c68ebe1c: suppress theories from other sessions, unless explicitly specified via…Jun 6 2021, 9:17 PM
makariusrISABELLE9ead8d9be3ab: clarified hook for Mirabelle: provide all loaded theories at once (for each…Jun 6 2021, 8:29 PM
florian.haftmannrISABELLE0510c7a4256a: moved more legacy to AFPJun 6 2021, 5:49 PM
florian.haftmannrAFP0b37c282b057: moved more legacy to AFPJun 6 2021, 5:49 PM
makariusrISABELLE745e2cd1f5f5: refer to theory "segments" only, according to global Build.build_theories and…Jun 6 2021, 4:34 PM
makariusrISABELLE60214976d846: tuned;Jun 6 2021, 2:55 PM
makariusrISABELLEd67688992bde: more uniform schedule_theories, notably for "present" and "commit" phase after…Jun 6 2021, 2:52 PM
makariusrISABELLEdf0fd744e6bb: tuned;Jun 6 2021, 2:12 PM
kleingrAFP98a8bdb85f79: merge from afp-2021Jun 6 2021, 3:06 AM