isabelle: Graph

updated to jdk-11;
2018-10-06, by wenzelm
generalization due to Alexander Maletzky
2018-10-06, by nipkow
discontinue java.ext.dirs for jdk-11 -- in contrast to 982f0bf34804 for jdk-8;
2018-10-05, by wenzelm
more [simp]
2018-10-05, by nipkow
avoid TCP_NODELAY (in contrast to 18c621069bf8): might cause problems with some versions of Ubuntu 18.04;
2018-10-04, by wenzelm
merged
2018-10-04, by paulson
updates to Algebra from Baillon and de Vilhena
2018-10-04, by paulson
use correct hostname
2018-10-04, by Lars Hupel
Jenkins: detect machine; adjust job parameters accordingly
2018-10-04, by Lars Hupel
Jenkins: tuned profiles
2018-10-04, by Lars Hupel
merged
2018-10-04, by nipkow
simplified proofs
2018-10-04, by nipkow
Jenkins: delete obsolete profile
2018-10-04, by Lars Hupel
tuned
2018-10-03, by nipkow
merged
2018-10-03, by wenzelm
unused -- avoid illegal access in Java 11;
2018-10-03, by wenzelm
misc tuning and modernization;
2018-10-03, by wenzelm
merged
2018-10-03, by paulson
merged
2018-09-24, by paulson
cosmetic change to mvt
2018-09-24, by paulson
shuffle -> shuffles
2018-10-03, by nipkow
shuffle -> shuffles
2018-10-03, by nipkow
updated windows_app to launch4j 3.12: "fully supports Java 9 and newer";
2018-10-02, by wenzelm
explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;
2018-10-02, by wenzelm
reduce tracing messages to make it work in PIDE session;
2018-10-02, by wenzelm
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
2018-10-02, by wenzelm
tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
2018-10-01, by wenzelm
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
2018-10-01, by wenzelm
tuned;
2018-10-01, by wenzelm
HOL-SPARK .prv files are no longer written to the file-system;
2018-10-01, by wenzelm
updated to postgresql-42.2.5;
2018-10-01, by wenzelm
merged
2018-09-30, by immler
fix (non-existent) document generation
2018-09-29, by immler
updated to scala-2.12.7;
2018-09-30, by wenzelm
news
2018-09-30, by nipkow
de-emphasize HOL-SPARK: somewhat outdated;
2018-09-30, by wenzelm
proper naming conventions for contexts;
2018-09-30, by wenzelm
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
2018-09-30, by wenzelm
tuned spelling;
2018-09-30, by wenzelm
tuned whitespace and sections;
2018-09-30, by wenzelm
tuned -- eliminated clone;
2018-09-30, by wenzelm
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
2018-09-30, by wenzelm
obsolete (see 6f8ae6ddc26b);
2018-09-30, by wenzelm
updated to new list_update precedence
2018-09-30, by nipkow
avoid confusing precedences
2018-09-30, by nipkow
more direct locale goal: avoid renaming of type_parameters;
2018-09-29, by wenzelm
adapted to Library/LaTeXsugar
2018-09-29, by nipkow
const_typ also works for fixed variables - useful primarily for locales
2018-09-29, by nipkow
tuned message according to ML version;
2018-09-29, by wenzelm
more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;
2018-09-29, by wenzelm
more accurate syntax: e.g. avoid brackets as prefix notation;
2018-09-28, by wenzelm
more approximative prefix syntax, including binder;
2018-09-28, by wenzelm
proper syntax for locale vs. class parameters;
2018-09-28, by wenzelm
simpler def
2018-09-27, by nipkow
tuned signature;
2018-09-26, by wenzelm
tuned signature;
2018-09-26, by wenzelm
provide CakeML component
2018-09-26, by Lars Hupel
clarified get_infix: avoid old ASCII input syntax;
2018-09-26, by wenzelm
remove dubious import
2018-09-26, by Lars Hupel
export locale dependencies, with approx. morphism as type/term substitution;
2018-09-25, by wenzelm
tuned signature;
2018-09-25, by wenzelm
merged
2018-09-24, by nipkow
NEWS
2018-09-24, by nipkow
more conversion from ( * ) to (*)
2018-09-24, by nipkow
Prefix form of infix with * on either side no longer needs special treatment
2018-09-24, by nipkow
expose locale_dependency information;
2018-09-24, by wenzelm
tuned signature;
2018-09-24, by wenzelm
tuned signature: more explicit types;
2018-09-24, by wenzelm
tuned;
2018-09-24, by wenzelm
tuned signature: prefer value-oriented pretty-printing;
2018-09-24, by wenzelm
tuned signature;
2018-09-24, by wenzelm
tuned signature: prefer value-oriented pretty-printing;
2018-09-24, by wenzelm
tuned (according to signature);
2018-09-24, by wenzelm
tuned comments: local context is intended according to 06fd1914b902 and documentation for command 'print_interps';
2018-09-24, by wenzelm
misc tuning and modernization;
2018-09-24, by wenzelm
more position information;
2018-09-24, by wenzelm
clarified message;
2018-09-24, by wenzelm
tuned signature: more explicit types;
2018-09-24, by wenzelm
clarified signature;
2018-09-24, by wenzelm
eliminated dead code (see b806a7678083);
2018-09-24, by wenzelm
tuned -- removed spurious dead code from 7b9a67cbd48f;
2018-09-24, by wenzelm
tuned signature: canonical argument order;
2018-09-24, by wenzelm
tuned signature;
2018-09-24, by wenzelm
discontinued old-style goal cases;
2018-09-23, by wenzelm
tuned;
2018-09-23, by wenzelm
more robust: logic image might be absent in PIDE session;
2018-09-23, by wenzelm
discontinued old-style inner comments;
2018-09-23, by wenzelm
tuned;
2018-09-23, by wenzelm
eliminated old-style inner comments;
2018-09-23, by wenzelm
More standard precedences
2018-09-23, by nipkow
more standard syntax
2018-09-23, by nipkow
News
2018-09-23, by nipkow
use standard syntax
2018-09-23, by nipkow
proper status after commit;
2018-09-22, by wenzelm
obsolete (see aec64b88e708);
2018-09-22, by wenzelm
proper return code for runtime failure;
2018-09-22, by wenzelm
clarified errors: no result from forced session.stop, check pending theories;
2018-09-22, by wenzelm
merged
2018-09-21, by paulson
more on product (function) topologies
2018-09-21, by paulson
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
2018-09-21, by wenzelm
clarified error;
2018-09-21, by wenzelm
clarified errors;
2018-09-21, by wenzelm
suppress some theories to allow "isabelle dump -o skip_proofs";
2018-09-21, by wenzelm
tuned signature;
2018-09-21, by wenzelm
merged
2018-09-20, by wenzelm
clarified standardization of variables, with proper treatment of local variables;
2018-09-20, by wenzelm
removal of more redundancies, and fixes
2018-09-20, by paulson
merged
2018-09-20, by paulson
elimination of near duplication involving Rolle's theorem and the MVT
2018-09-20, by paulson
export semi-unfolded locale axioms;
2018-09-19, by wenzelm
tuned;
2018-09-19, by wenzelm
clarified signature;
2018-09-19, by wenzelm
tuned signature;
2018-09-19, by wenzelm
more generous timeout: avoid sporadic failure in highly parallel headless PIDE session;
2018-09-18, by wenzelm
tuned signature;
2018-09-18, by wenzelm
tuned signature;
2018-09-18, by wenzelm
clarified modules;
2018-09-18, by wenzelm
merged
2018-09-17, by wenzelm
tuned message;
2018-09-17, by wenzelm
tuned message;
2018-09-17, by wenzelm
more detailed session dependencies, with conditions for theories;
2018-09-17, by wenzelm
clarified signature;
2018-09-17, by wenzelm
merged
2018-09-17, by nipkow
added insertion sort with keys
2018-09-17, by nipkow
Set idioms theory "finite intersection_of open", etc.
2018-09-17, by paulson
export plain infix syntax;
2018-09-16, by wenzelm
unused;
2018-09-16, by wenzelm
merged
2018-09-16, by paulson
more lemmas
2018-09-16, by paulson
tuned
2018-09-16, by nipkow
more traditional formulation
2018-09-16, by nipkow
more exports;
2018-09-15, by wenzelm
updated to Ubuntu 18.04;
2018-09-15, by wenzelm
merged
2018-09-14, by wenzelm
tuned;
2018-09-13, by wenzelm
added quicksort
2018-09-14, by nipkow
tuned
2018-09-14, by nipkow
more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
2018-09-13, by wenzelm
removed redundant lemma
2018-09-13, by nipkow
merged
2018-09-13, by nipkow
more simp lemmas
2018-09-13, by nipkow
tuned signature;
2018-09-13, by wenzelm
tuned message;
2018-09-13, by wenzelm
prefer explicit
2018-09-13, by nipkow
merged
2018-09-13, by nipkow
typo
2018-09-13, by nipkow
merged
2018-09-12, by wenzelm
tuned signature;
2018-09-12, by wenzelm
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
2018-09-12, by nipkow
merged
2018-09-12, by paulson
merged
2018-09-12, by paulson
tiny cleanup
2018-09-12, by paulson
merged
2018-09-11, by paulson
A few new results, elimination of duplicates and more use of "pairwise"
2018-09-11, by paulson
tuned
2018-09-12, by nipkow
tuned "=" syntax declarations; made "~=" uniformly "infix"
2018-09-12, by nipkow
tuned proof
2018-09-11, by nipkow
simplified defns
2018-09-11, by nipkow
"undefined" not needed, [] is perfectly natural
2018-09-11, by nipkow
tuned
2018-09-11, by nipkow
tuned
2018-09-10, by nipkow
tuned
2018-09-10, by nipkow
tuned
2018-09-10, by nipkow
Removed problematic rules from continuous_intros
2018-09-09, by eberlm
merged
2018-09-09, by nipkow
tuned
2018-09-09, by nipkow
tuned message (again);
2018-09-09, by wenzelm
proper binding positions within the defining command transaction;
2018-09-09, by wenzelm
smash position to avoid position of other file "~~/src/HOL/BNF_Composition.thy" (due to "bnf ID"), e.g. relevant for "HOL-Nominal-Examples.Class1";
2018-09-09, by wenzelm
clarified message;
2018-09-09, by wenzelm
tuned message;
2018-09-09, by wenzelm
clarified theory progress;
2018-09-09, by wenzelm
tuned message;
2018-09-08, by wenzelm
more robust test: virtualization may provide misleading information;
2018-09-08, by wenzelm
implicit use of NUMA policy, absorbing potential errors;
2018-09-08, by wenzelm
tuned signature;
2018-09-08, by wenzelm
tuned;
2018-09-08, by wenzelm
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
2018-09-08, by wenzelm
merged
2018-09-08, by wenzelm
ensure foundational order of commits, taking Pure as implicit starting point;
2018-09-08, by wenzelm
more accurate output;
2018-09-08, by wenzelm
clarified defaults;
2018-09-08, by wenzelm
more accurate output;
2018-09-08, by wenzelm
support for watchdog_timeout;
2018-09-08, by wenzelm
tuned signature;
2018-09-08, by wenzelm
tuned signature;
2018-09-08, by wenzelm
removed junk;
2018-09-08, by wenzelm
tuned output;
2018-09-08, by wenzelm
more appropriate conversion of HOL character literals to character codes: symbolic newline is interpreted as 0x10
2018-09-08, by haftmann
more explicit notion of ord value for HOL characters
2018-09-08, by haftmann
left-over rename from 3f9bb52082c4
2018-09-08, by haftmann
merged
2018-09-07, by wenzelm
continuously clean frontier of already committed theories: much less resource requirements;
2018-09-07, by wenzelm
tuned signature;
2018-09-07, by wenzelm
missing name
2018-09-07, by nipkow
tuned whitespace;
2018-09-07, by wenzelm
merged
2018-09-07, by wenzelm
proper tast_context (amending 5f44ad150ed8);
2018-09-07, by wenzelm
clarified error progress and error_rc;
2018-09-07, by wenzelm
tuned signature;
2018-09-07, by wenzelm
clarified rc;
2018-09-07, by wenzelm
tuned signature;
2018-09-07, by wenzelm
dump aspects asynchronously;
2018-09-07, by wenzelm
record status of already committed nodes;
2018-09-07, by wenzelm
tuned;
2018-09-07, by wenzelm
tuned signature;
2018-09-07, by wenzelm
tuned;
2018-09-07, by wenzelm
added Let_def
2018-09-07, by nipkow
merged
2018-09-06, by nipkow
added int and real
2018-09-06, by nipkow
simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
2018-09-06, by wenzelm
setup option ML_system for special values that cannot be rebound within regular ML;
2018-09-06, by wenzelm
support dynamic commit of consilidated nodes;
2018-09-05, by wenzelm
tuned signature;
2018-09-05, by wenzelm
clarified Use_Theories_State;
2018-09-05, by wenzelm
tuned
2018-09-05, by nipkow
merged
2018-09-05, by nipkow
tuned doc
2018-09-05, by nipkow
proper binding position for the resulting definition command, not this source file;
2018-09-04, by wenzelm
material on finite sets
2018-08-30, by Lars Hupel
support for watchdog_timeout;
2018-09-04, by wenzelm
tuned;
2018-09-04, by wenzelm
tuned;
2018-09-04, by wenzelm
tuned -- prefer immutable data;
2018-09-04, by wenzelm
tuned signature;
2018-09-04, by wenzelm
clarified Nodes_Status;
2018-09-04, by wenzelm
tuned
2018-09-04, by nipkow
tuned
2018-09-03, by nipkow
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
2018-09-03, by wenzelm
more detailed progress;
2018-09-03, by wenzelm
more informative node_status;
2018-09-03, by wenzelm
tuned signature;
2018-09-03, by wenzelm
more robust default options, notably for node consolidation;
2018-09-03, by wenzelm
tuned;
2018-09-03, by wenzelm
more robust: load_theories after consumer is installed;
2018-09-03, by wenzelm
merged
2018-09-03, by wenzelm
proper polarity of terminated status;
2018-09-03, by wenzelm
merged
2018-09-03, by Angeliki KoutsoukouArgyraki
tagged 1 theory: Great_Picard
2018-09-03, by Angeliki KoutsoukouArgyraki
tuned signature;
2018-09-02, by wenzelm