13 months ago wenzelm clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
13 months ago wenzelm unused;
13 months ago wenzelm enforce rebuild of Isabelle/Scala + Isabelle/ML;
13 months ago wenzelm updated to postgresql-42.7.1;
13 months ago wenzelm updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;
13 months ago wenzelm update to llncs-2.23;
13 months ago wenzelm clarified bootstrap;
13 months ago wenzelm clarified directories;
13 months ago wenzelm clarified directories;
13 months ago wenzelm obsolete (see also fc88b943e1b2);
13 months ago wenzelm proper output, following 2cd23d587db9;
13 months ago wenzelm always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
13 months ago wenzelm clarified directories;
13 months ago wenzelm more accurate Isabelle versions;
13 months ago wenzelm more accurate Ubuntu versions;
13 months ago nipkow more uses of define_time_fun
13 months ago nipkow translation to time functions now with canonical let.
13 months ago paulson merged
13 months ago paulson A few new results (mostly brought in from other developments)
13 months ago nipkow merged
13 months ago nipkow Added time function automation
13 months ago haftmann streamlined type class specification
13 months ago haftmann consolidated lemma name
13 months ago wenzelm support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
13 months ago wenzelm merged
13 months ago wenzelm tuned;
13 months ago wenzelm update links;
13 months ago wenzelm follow post-maintenance updates of original Phabricator, as base-line for Phorge;
13 months ago wenzelm refer to "localhost" as pro-forma domain;
13 months ago haftmann simplified specification of type class
13 months ago haftmann consolidated name of lemma analogously to nat/int/word_bit_induct
13 months ago wenzelm more accurate syntax: 'obtain' vars are optional;
13 months ago wenzelm clarified order, disregard structure of proof;
13 months ago wenzelm minor performance tuning;
13 months ago wenzelm tuned;
13 months ago wenzelm more thorough treatment of hidden type variables within zproof;
13 months ago wenzelm more uniform treatment of "hyps" within zproof;
13 months ago wenzelm clarified order: follow Thm.fold_terms;
13 months ago wenzelm merged
13 months ago wenzelm clarified signature;
13 months ago wenzelm clarified signature;
13 months ago wenzelm tuned signature;
13 months ago wenzelm tuned;
13 months ago wenzelm clarified test: no exception yet;
13 months ago wenzelm tuned;
13 months ago wenzelm tuned;
13 months ago wenzelm tuned signature: more direct operations;
13 months ago wenzelm clarified signature;
13 months ago wenzelm clarified signature: more direct operations;
13 months ago wenzelm tuned signature;
13 months ago wenzelm tuned;
13 months ago wenzelm minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
13 months ago wenzelm tuned whitespace;
13 months ago wenzelm more robust: certify types uniformly (see also 62b75508eb66);
13 months ago wenzelm tuned;
13 months ago wenzelm clarified signature;
13 months ago wenzelm clarified signature: avoid redundant Term.maxidx_of_term;
13 months ago wenzelm proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
13 months ago wenzelm misc tuning and clarification: prefer Same.operation;
13 months ago wenzelm clarified signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip