Page MenuHomePhabricator
Feed All Stories

Today

paulson <lp15@cam.ac.uk> committed rISABELLEec7cc76e88e5: New library material from the AFP entry ZFC_in_HOL.
New library material from the AFP entry ZFC_in_HOL
Tue, Nov 12, 1:35 PM

Yesterday

haftmann committed rISABELLE038727567817: tuned order between theories.
tuned order between theories
Mon, Nov 11, 7:37 PM

Sun, Nov 10

haftmann committed rISABELLEa197532693a5: bit shifts as class operations.
bit shifts as class operations
Sun, Nov 10, 2:48 PM
haftmann committed rISABELLEb7d481cdd54d: new lemma.
new lemma
Sun, Nov 10, 2:48 PM
Lars Hupel <lars.hupel@mytum.de> committed rAFPf1ef07c47429: don't build Linear_Programming on Mac.
don't build Linear_Programming on Mac
Sun, Nov 10, 1:20 PM

Fri, Nov 8

wenzelm committed rISABELLE3c04a52c422a: tuned comments;.
tuned comments;
Fri, Nov 8, 9:48 PM
wenzelm committed rISABELLEfd82d53c1761: merged.
merged
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLE06c6495fb1d0: retain type information from reconstruct_proof, notably for Export_Theory..
retain type information from reconstruct_proof, notably for Export_Theory.
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLE4b45d592ce29: clarified modules;.
clarified modules;
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLE907b7a6471a0: tuned proofs;.
tuned proofs;
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLE77580c977e0c: more robust;.
more robust;
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLEaedd11603fb4: tuned modules;.
tuned modules;
Fri, Nov 8, 8:51 PM
wenzelm committed rISABELLE950e1cfe0fe4: tuned proofs -- more stable proof terms without [rule_format];.
tuned proofs -- more stable proof terms without [rule_format];
Fri, Nov 8, 8:51 PM
paulson committed rISABELLEc4458eb355c0: merged.
merged
Fri, Nov 8, 5:18 PM
paulson <lp15@cam.ac.uk> committed rISABELLEce92360f0692: A slight tidying up of messy proof steps.
A slight tidying up of messy proof steps
Fri, Nov 8, 5:18 PM

Thu, Nov 7

wenzelm committed rISABELLE995fe5877d53: tuned declarations for more compact proof terms;.
tuned declarations for more compact proof terms;
Thu, Nov 7, 4:31 PM
wenzelm committed rISABELLE45a1fcee14a0: prefer named facts;.
prefer named facts;
Thu, Nov 7, 4:31 PM
wenzelm committed rISABELLE64249a83bc29: clarified contexts;.
clarified contexts;
Thu, Nov 7, 4:31 PM
wenzelm committed rISABELLEe06852132c1d: tuned messages;.
tuned messages;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE5bb2235d843d: clarified command-line;.
clarified command-line;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE41b6ca223500: tuned messages;.
tuned messages;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE8ac137c65776: tuned messages;.
tuned messages;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE70205e023cb4: more messages -- expose potential database problems;.
more messages -- expose potential database problems;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE324c40205fc8: clarified errors: include stdout;.
clarified errors: include stdout;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLEd61fd7aade69: clarified directory;.
clarified directory;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE22fcdadc404d: tuned;.
tuned;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE9ce299019d21: tuned message;.
tuned message;
Thu, Nov 7, 11:59 AM
wenzelm committed rISABELLE79b89278b825: clarified permissions;.
clarified permissions;
Thu, Nov 7, 11:59 AM

Wed, Nov 6

wenzelm committed rISABELLE9314a4cc84ea: merged.
merged
Wed, Nov 6, 11:55 PM
wenzelm committed rISABELLE510b89906d86: discontinued somewhat pointless Isabelle options: setup implicitly assumes….
discontinued somewhat pointless Isabelle options: setup implicitly assumes…
Wed, Nov 6, 11:55 PM
wenzelm committed rISABELLE67cbf2e52785: unused;.
unused;
Wed, Nov 6, 11:55 PM
wenzelm committed rISABELLE114db2b5a5f8: support for Phabricator mail configuration;.
support for Phabricator mail configuration;
Wed, Nov 6, 11:55 PM
traytel committed rISABELLE98ac9a4323a2: merged.
merged
Wed, Nov 6, 9:24 PM
traytel committed rISABELLEc9c1a64eeb69: corrected typo in lemma name.
corrected typo in lemma name
Wed, Nov 6, 9:24 PM
nipkow committed rISABELLEd628bbdce79a: moved lemma.
moved lemma
Wed, Nov 6, 7:17 PM
traytel committed rISABELLEb3956a37c994: merged.
merged
Wed, Nov 6, 4:39 PM
traytel committed rISABELLE1d19e844fa4d: characterization of until in terms of strong until (and vice versa)….
characterization of until in terms of strong until (and vice versa)…
Wed, Nov 6, 4:39 PM
nipkow committed rISABELLE295609359b58: tuned toc.
tuned toc
Wed, Nov 6, 11:09 AM

Tue, Nov 5

nipkow committed rAFP54f6a4f1d8a3: updated to fdb6c5034c24.
updated to fdb6c5034c24
Tue, Nov 5, 11:54 PM
immler committed rAFP2a06a089800f: merged.
merged
Tue, Nov 5, 11:54 PM
paulson <lp15@cam.ac.uk> committed rAFP3f2bdb753c38: patched a proof.
patched a proof
Tue, Nov 5, 11:54 PM
immler committed rAFPc5944c920143: moved Interval and Interval_Approximation to isabelle.
moved Interval and Interval_Approximation to isabelle
Tue, Nov 5, 11:53 PM
wenzelm committed rISABELLE9b531e611d66: merged.
merged
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE2965304143d8: more phabricator setup;.
more phabricator setup;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE6ca9e8377613: proper names for multiple installations;.
proper names for multiple installations;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLEee3c43eb79ae: proper service name (again): it is specific to each installation;.
proper service name (again): it is specific to each installation;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLEb64fc38327ae: prefer system user setup, e.g. avoid occurrence on login screen;.
prefer system user setup, e.g. avoid occurrence on login screen;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE27a998cdc0f4: back to plain name, to have it accepted my mysql;.
back to plain name, to have it accepted my mysql;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLEba14aa0b5a5d: more robust: install PHP daemon after Apache;.
more robust: install PHP daemon after Apache;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE6bf53035baf0: clarified name prefixes: global config always uses "isabelle-phabricator";.
clarified name prefixes: global config always uses "isabelle-phabricator";
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE8198ceef0301: more phabricator setup;.
more phabricator setup;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE4eeff87c5072: more phabricator setup;.
more phabricator setup;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLEf4b9dd5ab0cc: more phabricator setup;.
more phabricator setup;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE5f02ecbb19d6: support for system services;.
support for system services;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLE87c132cf5860: more options;.
more options;
Tue, Nov 5, 11:10 PM
wenzelm committed rISABELLEb8aeeedf7e68: support for Linux user management;.
support for Linux user management;
Tue, Nov 5, 11:10 PM
nipkow committed rISABELLE9858f391ed2d: merged.
merged
Tue, Nov 5, 9:17 PM
nipkow committed rISABELLEcb504351d058: tuned.
tuned
Tue, Nov 5, 9:17 PM
nipkow committed rISABELLE2fab72ab919a: moved duplicate lemmas up the hierarchy.
moved duplicate lemmas up the hierarchy
Tue, Nov 5, 9:17 PM
haftmann committed rISABELLE400e9512f1d3: proof-of-concept theory for bit operations without a constructivistic….
proof-of-concept theory for bit operations without a constructivistic…
Tue, Nov 5, 7:22 PM
nipkow committed rISABELLEfdb6c5034c24: merged.
merged
Tue, Nov 5, 7:15 PM
nipkow committed rISABELLE9d2753406c60: removed redundant lemma.
removed redundant lemma
Tue, Nov 5, 7:15 PM
immler committed rISABELLEddd4aefc540f: merged.
merged
Tue, Nov 5, 4:09 PM
immler committed rISABELLEbd3d4702b4f2: add lemmas.
add lemmas
Tue, Nov 5, 4:09 PM
immler committed rISABELLEf630f2e707a6: refactor Approximation.thy to use more abstract type of intervals.
refactor Approximation.thy to use more abstract type of intervals
Tue, Nov 5, 4:09 PM
immler committed rISABELLEdfcc1882d05a: moved theory Interval_Approximation from the AFP.
moved theory Interval_Approximation from the AFP
Tue, Nov 5, 4:09 PM
immler committed rISABELLE6fe5a0e1fa8e: moved theory Interval from the AFP.
moved theory Interval from the AFP
Tue, Nov 5, 4:09 PM
immler committed rISABELLEe0755162093f: replace approximation oracle by less ad-hoc @{computation}s.
replace approximation oracle by less ad-hoc @{computation}s
Tue, Nov 5, 4:09 PM
nipkow committed rISABELLEc1b63124245c: tuned.
tuned
Tue, Nov 5, 2:57 PM
nipkow committed rISABELLEacedd04c1a42: merged.
merged
Tue, Nov 5, 2:09 PM
nipkow committed rISABELLE66c025383422: tuned.
tuned
Tue, Nov 5, 2:09 PM
paulson <lp15@cam.ac.uk> committed rISABELLEb6e69c71a9f6: Merge and get rid of closed_segmentI.
Merge and get rid of closed_segmentI
Tue, Nov 5, 1:01 PM
paulson <lp15@cam.ac.uk> committed rISABELLE934e0044e94b: Moved or deleted some out of place material, also eliminating obsolete naming….
Moved or deleted some out of place material, also eliminating obsolete naming…
Tue, Nov 5, 1:01 PM
immler committed rISABELLEc2465b429e6e: Line_Segment is independent of Convex_Euclidean_Space.
Line_Segment is independent of Convex_Euclidean_Space
Tue, Nov 5, 3:42 AM
immler committed rISABELLEb212ee44f87c: the division between Starlike and Convex_Euclidean_Space is artificial….
the division between Starlike and Convex_Euclidean_Space is artificial…
Tue, Nov 5, 2:01 AM
immler committed rISABELLE12cbcd00b651: betweenness is a property on line segments.
betweenness is a property on line segments
Tue, Nov 5, 2:01 AM
immler committed rISABELLEbe8cec1abcbb: reduce dependencies of Ordered_Euclidean_Space; move more general material from….
reduce dependencies of Ordered_Euclidean_Space; move more general material from…
Tue, Nov 5, 2:01 AM

Mon, Nov 4

wenzelm committed rISABELLE35a8e15b7e03: more robust Thm.expose_theory -- ensure that PIDE export happens in the proper….
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper…
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLE38bed2483e6a: proper message (amending 94442fce40a5);.
proper message (amending 94442fce40a5);
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLEb697dd74221a: tuned;.
tuned;
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLE6504ea98623c: uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with….
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with…
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLE4003da7e6a79: updated xml_size;.
updated xml_size;
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLEc9f5f724abc0: prefer named result;.
prefer named result;
Mon, Nov 4, 8:54 PM
wenzelm committed rISABELLEd32ed8927a42: more robust expose_proofs corresponding to register_proofs/consolidate_theory;.
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
Mon, Nov 4, 8:54 PM

Sun, Nov 3

wenzelm committed rISABELLEc85efa2be619: expose derivations more thoroughly, notably for locale/class reasoning;.
expose derivations more thoroughly, notably for locale/class reasoning;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLEbb49abc2ecbb: determine proof boxes from exported proof (NB: thm_boxes is not sufficient due….
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due…
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLEb05d78bfc67c: clarified errors;.
clarified errors;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLE58022ee70b35: more operations;.
more operations;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLEbfa1017b4553: tuned whitespace;.
tuned whitespace;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLE73f14e0b7151: more robust;.
more robust;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLE2c96e48027eb: clarified modules;.
clarified modules;
Sun, Nov 3, 8:59 PM
wenzelm committed rISABELLEbe689b7d81fd: clarified signature -- more options;.
clarified signature -- more options;
Sun, Nov 3, 8:59 PM
paulson committed rISABELLEbb403cb94db2: merged.
merged
Sun, Nov 3, 11:46 AM
paulson <lp15@cam.ac.uk> committed rISABELLEe892f7a1fd83: moved line segments to Convex_Euclidean_Space.
moved line segments to Convex_Euclidean_Space
Sun, Nov 3, 11:46 AM

Sat, Nov 2

wenzelm committed rISABELLE15129c2f4a33: proper theory for export_proofs;.
proper theory for export_proofs;
Sat, Nov 2, 11:56 PM
wenzelm committed rISABELLE41685289b8eb: tuned signature;.
tuned signature;
Sat, Nov 2, 11:56 PM
paulson committed rISABELLE7f1241a2bf30: merged.
merged
Sat, Nov 2, 9:53 PM
paulson <lp15@cam.ac.uk> committed rISABELLEb86d30707837: just tidied one proof.
just tidied one proof
Sat, Nov 2, 9:53 PM
wenzelm committed rISABELLE699ff83813c0: proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);.
proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);
Sat, Nov 2, 9:10 PM
paulson <lp15@cam.ac.uk> committed rAFPc5c88012f116: fixed a failing (and ugly) proof.
fixed a failing (and ugly) proof
Sat, Nov 2, 8:26 PM