isabelle: Graph

clarified signature;
2020-06-27, by wenzelm
more CONTRIBUTORS;
2020-06-26, by wenzelm
more uniform URL (see 60b5a4731695);
2020-06-25, by wenzelm
clarified use of memory: prefer share tree structures over fresh strings;
2020-06-24, by wenzelm
more Java heap space (see 2d658beb815b);
2020-06-24, by wenzelm
clarified NEWS;
2020-06-21, by wenzelm
enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
2020-06-20, by wenzelm
discontinued old AFP test: ancient hardware with insufficient resources;
2020-06-20, by wenzelm
tuned output;
2020-06-20, by wenzelm
merged
2020-06-20, by wenzelm
share cache for parallel sessions;
2020-06-20, by wenzelm
clarified signature;
2020-06-20, by wenzelm
more caching, notably for build/pide_session;
2020-06-20, by wenzelm
removed pointless pide_exports: unused during "build_session" process (reverting 6a64205b491a);
2020-06-20, by wenzelm
tuned --- avoid error in IntelliJ IDEA;
2020-06-19, by wenzelm
simp rules for conversions
2020-06-20, by haftmann
more class operations for the sake of efficient generated code
2020-06-20, by haftmann
merged
2020-06-19, by wenzelm
back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
2020-06-19, by wenzelm
back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);
2020-06-19, by wenzelm
clarified signature;
2020-06-19, by wenzelm
avoid redundant export handling for build;
2020-06-19, by wenzelm
prefer single name
2020-06-19, by haftmann
more lemmas
2020-06-18, by haftmann
build bit operations on word on library theory on bit operations
2020-06-18, by haftmann
bit operations as distinctive library theory
2020-06-18, by haftmann
tweak for code generation
2020-06-18, by haftmann
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
2020-06-18, by haftmann
more lemmas and less name space pollution
2020-06-18, by haftmann
canonical bit shifts for word type, leaving duplicates as they are at the moment
2020-06-18, by haftmann
essential instance about bit structure
2020-06-18, by haftmann
more transfer rules
2020-06-18, by haftmann
dropped yet another duplicate
2020-06-18, by haftmann
fundamental construction of word type following existing transfer rules
2020-06-18, by haftmann
replaced mere alias by input abbreviation
2020-06-18, by haftmann
replaced mere alias by abbreviation
2020-06-18, by haftmann
replaced operation with weak abstraction by input abbreviation
2020-06-18, by haftmann
avoid compound operation
2020-06-18, by haftmann
formal relationships between operations
2020-06-18, by haftmann
eliminated warnings
2020-06-18, by haftmann
replaced mere alias by input abbreviation
2020-06-18, by haftmann
enable pide_session by default;
2020-06-17, by wenzelm
avoid resource problems of JVM by too many parallel XZ compression tasks;
2020-06-17, by wenzelm
interpretations for boolean operators
2020-06-16, by haftmann
more specific thm reference
2020-06-16, by haftmann
clarified errors;
2020-06-13, by wenzelm
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
2020-06-11, by paulson
tuned whitespace;
2020-06-11, by wenzelm
proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
2020-06-11, by wenzelm
updated to jedit-5.6pre1 (repository version 25349);
2020-06-10, by wenzelm
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
2020-06-10, by blanchet
New Ackermann development
2020-06-09, by paulson
tuned document;
2020-06-08, by wenzelm
proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;
2020-06-08, by wenzelm
NEWS;
2020-06-08, by wenzelm
clarified sessions;
2020-06-08, by wenzelm
clarified sessions: "Notable Examples in Isabelle/HOL";
2020-06-08, by wenzelm
clarified sessions: "Notable Examples in Isabelle/Pure";
2020-06-08, by wenzelm
NEWS
2020-06-06, by haftmann
more theorems
2020-06-04, by haftmann
avoid overaggressive default simp rules
2020-06-04, by haftmann
activate simproc for FOL
2020-06-04, by haftmann
more rules for FOL also
2020-06-04, by haftmann
more simp rules
2020-06-04, by haftmann
should have been copied across from Set.thy as well for better printing
2020-06-03, by nipkow
specific atomization inert to later rule set modifications
2020-05-30, by haftmann
more precise scope of atomize
2020-05-30, by haftmann
install simproc but deactivate by default
2020-05-30, by haftmann
adapted to d25093536482;
2020-05-27, by wenzelm
clarified markup;
2020-05-27, by wenzelm
clarified signature;
2020-05-27, by wenzelm
tuned signature;
2020-05-27, by wenzelm
tuned;
2020-05-27, by wenzelm
more NEWS;
2020-05-27, by wenzelm
more documentation on Isabelle/Scala;
2020-05-27, by wenzelm
proper error positions;
2020-05-27, by wenzelm
tuned;
2020-05-27, by wenzelm
tuned whitespace;
2020-05-27, by wenzelm
more antiquotations;
2020-05-27, by wenzelm
check bash functions against Isabelle settings environment;
2020-05-27, by wenzelm
misc tuning;
2020-05-27, by wenzelm
breakable scala_name;
2020-05-27, by wenzelm
tuned signature;
2020-05-26, by wenzelm
discontinued pointless document antiquotation;
2020-05-26, by wenzelm
proper check of example;
2020-05-26, by wenzelm
clarified signature --- fit within limit of 22 arguments;
2020-05-26, by wenzelm
tuned;
2020-05-26, by wenzelm
tuned;
2020-05-26, by wenzelm
more antiquotations;
2020-05-25, by wenzelm
obsolete;
2020-05-25, by wenzelm
check free-form Scala source;
2020-05-25, by wenzelm
clarified static_check: avoid accidental evaluation;
2020-05-25, by wenzelm
omit pointless memoing: Scala compiler is rather bulky anyway;
2020-05-25, by wenzelm
clarified signature;
2020-05-25, by wenzelm
antiquotations for Scala entities;
2020-05-25, by wenzelm
better closeup and more consistent terminology
2020-05-24, by haftmann
merged
2020-05-24, by wenzelm
proper stack_limit;
2020-05-24, by wenzelm
clarified signature;
2020-05-24, by wenzelm
more accurate classpath for "isabelle scala";
2020-05-24, by wenzelm
proper check of registered Scala functions;
2020-05-24, by wenzelm
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
2020-05-24, by wenzelm
clarified build_session protocol;
2020-05-24, by wenzelm
clarified signature;
2020-05-24, by wenzelm
clarified name;
2020-05-24, by wenzelm
more robust: explicit check for PIDE session;
2020-05-24, by wenzelm
tuned signature;
2020-05-24, by wenzelm
unused;
2020-05-24, by wenzelm
tuned signature;
2020-05-23, by wenzelm
check Scala source snippets from ML;
2020-05-23, by wenzelm
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
2020-05-23, by wenzelm
init default context;
2020-05-23, by wenzelm
tuned message;
2020-05-23, by wenzelm
clarified signature;
2020-05-23, by wenzelm
tuned;
2020-05-23, by wenzelm
more brackets (see 2e8af171887f);
2020-05-23, by wenzelm
tuned message;
2020-05-23, by wenzelm
clarified signature;
2020-05-22, by wenzelm
unused;
2020-05-22, by wenzelm
more robust, notably for "isabelle scala";
2020-05-22, by wenzelm
clarified signature;
2020-05-22, by wenzelm
reorganised sorted_set_of_list
2020-05-24, by nipkow
merged
2020-05-24, by nipkow
simpler inductions
2020-05-24, by nipkow
a few new lemmas about functions
2020-05-23, by paulson
comment makes no sense
2020-05-22, by nipkow
added simp lemma
2020-05-22, by nipkow
slightly more specific implementations
2020-05-21, by haftmann
tuned module name space for generated code
2020-05-21, by haftmann
unused alias
2020-05-21, by nipkow
generalized and augmented
2020-05-20, by haftmann
clarified signature;
2020-05-20, by wenzelm
clarified modules;
2020-05-20, by wenzelm
A few new theorems, plus some tidying up
2020-05-20, by paulson
corrected spelling and tuned whitespace
2020-05-20, by haftmann
tuned
2020-05-19, by nipkow
follow Phabricator update 2020 Week 19;
2020-05-18, by wenzelm
another AVL tree version
2020-05-17, by nipkow
added missing preprocessing step for extraction (due to Stefan Berghofer)
2020-05-15, by Manuel Eberl
new HOL simproc: eliminate_false_implies
2020-05-13, by Manuel Eberl
added lemma
2020-05-14, by nipkow
Tuned some proofs in HOL-Analysis
2020-05-14, by Manuel Eberl
The Uniq quantifier for FOL too
2020-05-14, by paulson
generalised pigeonhole principle in HOL-Library.FuncSet
2020-05-13, by Manuel Eberl
new constant power_int in HOL
2020-05-13, by Manuel Eberl
New HOL simproc 'datatype_no_proper_subterm'
2020-05-04, by Manuel Eberl
merged
2020-05-12, by paulson
Fixes for Sup{} = (0::nat)
2020-05-12, by paulson
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
2020-05-12, by paulson
clarified session imports: avoid bulky HOL-Library image;
2020-05-12, by wenzelm
tuned -- avoid warning;
2020-05-12, by wenzelm
"app" -> "join" for RBTs
2020-05-12, by nipkow
"app" -> "join" for uniformity with Join theory; tuned defs
2020-05-12, by nipkow
added top-level functions and tuned
2020-05-11, by nipkow
the Uniq quantifier
2020-05-11, by paulson
modernized notation for bit operations
2020-05-09, by haftmann
merged
2020-05-08, by nipkow
avoid hidden undef cases
2020-05-08, by nipkow
explicit mask operation for bits
2020-05-08, by haftmann
prefer _ mod 2 over of_bool (odd _)
2020-05-08, by haftmann
less aggressive default simp rules
2020-05-08, by haftmann
simplified and tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned
2020-05-06, by nipkow
tuned proofs
2020-05-05, by nipkow
tuned var. names
2020-05-05, by nipkow
tuned var. names
2020-05-04, by nipkow
AVL trees with balance tags
2020-05-04, by nipkow
A little more tidying up
2020-04-29, by paulson
tuned
2020-04-29, by nipkow
merged
2020-04-28, by nipkow
tuned
2020-04-28, by nipkow
merged
2020-04-28, by wenzelm
added "isabelle sessions" tool;
2020-04-28, by wenzelm
tuned messages;
2020-04-28, by wenzelm
use abs(h l - h r) instead of 3 cases, tuned proofs
2020-04-28, by nipkow
added lemmas
2020-04-27, by nipkow
simplified construction of binary bit operations
2020-04-27, by haftmann
temporarily revert change which does not work as expected
2020-04-25, by haftmann
more rules
2020-04-25, by haftmann
added Height_Balanced_Trees
2020-04-25, by nipkow
documentation of relevant ideas
2020-04-24, by haftmann
numeral rules for take_bit / drop_bit on int
2020-04-24, by haftmann
opaque export does not work as expected in presence of dependent instances
2020-04-24, by haftmann
merged
2020-04-23, by nipkow
tuned document
2020-04-23, by nipkow
split AVL_Set.thy
2020-04-23, by nipkow
avoid passing chained facts twice to preplay in Sledgehammer
2020-04-23, by blanchet
tweaked Vampire's options + tuning
2020-04-23, by blanchet
more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);
2020-04-23, by wenzelm
back to more modest (but uniform) Java stack, see 97fc4f657bda;
2020-04-23, by wenzelm
more generous Java memory, also hoping to prevent spurious java.lang.StackOverflowError in isabelle_cronjob;
2020-04-23, by wenzelm
added lemmas
2020-04-23, by nipkow
hooks for foundational terms: protection of foundational terms during simplification
2020-04-21, by haftmann
merged
2020-04-22, by wenzelm
merged
2020-04-22, by wenzelm
avoid deprecated operations;
2020-04-22, by wenzelm
tuned -- avoid odd compiler warning;
2020-04-22, by wenzelm
avoid deprecated operations;
2020-04-22, by wenzelm
deprecated and obsolete;
2020-04-22, by wenzelm
tuned signature -- avoid warnings;
2020-04-22, by wenzelm
more informative error;
2020-04-22, by wenzelm
new funs successive and distinct_adj
2020-04-22, by nipkow
added lemmas
2020-04-22, by nipkow
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
2020-04-21, by wenzelm
clarified signature -- avoid warning;
2020-04-21, by wenzelm
tuned;
2020-04-21, by wenzelm
clarified imports;
2020-04-21, by wenzelm
more robust judgment handling
2020-04-20, by haftmann
Sketch and explore again
2020-04-19, by paulson
removal of symmetries in Polytope, plus some tidying
2020-04-19, by paulson
Sketch_and_Explore — oops
2020-04-19, by paulson
the rest of the applys
2020-04-19, by paulson
more applys
2020-04-18, by paulson
merged
2020-04-17, by paulson
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
2020-04-17, by paulson
discontinued somewhat incoherent patches (see also 3b36fc4916af);
2020-04-17, by wenzelm
use friendlier package;
2020-04-17, by wenzelm
removed LaTeX package and hack to avoid ALLCAPS headers
2020-04-17, by blanchet
use friendlier package
2020-04-17, by blanchet
move virtual machine node;
2020-04-16, by wenzelm
generalized
2020-04-16, by haftmann
more theorems
2020-04-16, by haftmann
another rule on numerals
2020-04-16, by haftmann
bit on numerals
2020-04-16, by haftmann
more complete rules on numerals
2020-04-16, by haftmann
more complete rules on numerals
2020-04-16, by haftmann
removed obsolete RC tags;
2020-04-16, by wenzelm
merged
2020-04-15, by wenzelm
Added tag Isabelle2020 for changeset abf3e80bd815
2020-04-15, by wenzelm
tuned NEWS; Isabelle2020
2020-04-13, by wenzelm
tuned NEWS;
2020-04-12, by wenzelm
tuned message;
2020-04-13, by wenzelm
tuned message;
2020-04-13, by wenzelm
clarified signature;
2020-04-13, by wenzelm
more cleaning up Homotopy
2020-04-12, by paulson
cleaning up Homotopy
2020-04-12, by paulson
merged
2020-04-10, by paulson
more removal of applys
2020-04-10, by paulson
avoid hard-wired stuff: configure via plugin services;
2020-04-09, by wenzelm
tuned;
2020-04-09, by wenzelm
tuned;
2020-04-09, by wenzelm
clarified init of settings vs. services;
2020-04-08, by wenzelm
tuned message;
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
another isabelle_scala_service;
2020-04-08, by wenzelm
tuned;
2020-04-08, by wenzelm
tuned -- avoid deprecated operations;
2020-04-08, by wenzelm
more general support for isabelle_scala_service;
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
merged
2020-04-08, by wenzelm
Added tag Isabelle2020-RC5 for changeset 8ed68b2aeba1
2020-04-08, by wenzelm
more robust: notably for sledgehammer with 'using' and prover=cvc4;
2020-04-04, by wenzelm
NEWS;
2020-04-07, by wenzelm
more careful handling of interrupts, notably for Isabelle/jEdit Scala Console;
2020-04-07, by wenzelm
clarified signature: more uniform treatment of stopped/interrupted state;
2020-04-07, by wenzelm