isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

tuned whitespace -- slightly more readable;
2019-08-08, by wenzelm
clarified signature: fewer warnings in ML IDE;
2019-08-08, by wenzelm
tuned;
2019-08-08, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-07, by wenzelm
more compact proofterms;
2019-08-07, by wenzelm
eliminated pointless comments;
2019-08-07, by wenzelm
clarified proofterms;
2019-08-07, by wenzelm
more robust and convenient treatment of implicit context;
2019-08-07, by wenzelm
removed junk (cf. fa933b98d64d);
2019-08-07, by wenzelm
explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
2019-08-07, by wenzelm
more careful treatment of implicit context;
2019-08-07, by wenzelm
more careful treatment of implicit context;
2019-08-07, by wenzelm
proper build options;
2019-08-07, by wenzelm
merged
2019-08-06, by wenzelm
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
2019-08-06, by wenzelm
more careful treatment of implicit context;
2019-08-06, by wenzelm
clarified signature;
2019-08-06, by wenzelm
more robust and convenient treatment of implicit context;
2019-08-06, by wenzelm
clarified context: proper transfer;
2019-08-06, by wenzelm
tuned;
2019-08-06, by wenzelm
clarified modules: more direct data implementation;
2019-08-05, by wenzelm
Added Takeuchi function to HOL-ex
2019-08-06, by Manuel Eberl
full AFP test on lrzcloud2;
2019-08-05, by wenzelm
obsolete;
2019-08-05, by wenzelm
more efficient data structure;
2019-08-03, by wenzelm
clarified signature;
2019-08-03, by wenzelm
guard constraints by record_proofs=1, until performance implications have become more clear;
2019-08-03, by wenzelm
more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;
2019-08-03, by wenzelm
tuned;
2019-08-03, by wenzelm
tuned;
2019-08-03, by wenzelm
maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
2019-08-03, by wenzelm
more direct proofs for type classes;
2019-08-02, by wenzelm
tuned;
2019-08-02, by wenzelm
clarified modules: inference kernel maintains sort algebra within the logic;
2019-08-02, by wenzelm
more elementary treatment of standard_vars (unconstrainT is already standard);
2019-08-01, by wenzelm
clarified module structure;
2019-08-01, by wenzelm
simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);
2019-08-01, by wenzelm
abstract type theory_id -- ensure non-equality type independently of implementation;
2019-08-01, by wenzelm
clarified export: retain proof boxes as local definitions -- more scalable;
2019-07-31, by wenzelm
reduced dependencies
2019-07-31, by nipkow
clarified global theory context;
2019-07-30, by wenzelm
more robust export, based on reconstruct_proof / expand_proof;
2019-07-30, by wenzelm
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
2019-07-30, by wenzelm
tuned -- fewer warnings;
2019-07-30, by wenzelm
discontinued pointless messages;
2019-07-30, by wenzelm
clarified context;
2019-07-30, by wenzelm
clarified modules;
2019-07-30, by wenzelm
discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;
2019-07-30, by wenzelm
merged
2019-07-29, by wenzelm
more diagnostic operations;
2019-07-29, by wenzelm
tuned -- non-strict args;
2019-07-29, by wenzelm
proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
2019-07-29, by wenzelm
tuned signature;
2019-07-29, by wenzelm
clarified signature;
2019-07-29, by wenzelm
tuned signature;
2019-07-29, by wenzelm
News for bind infixl
2019-07-29, by nipkow
Monadic bind is now infixl as is the norm
2019-07-29, by nipkow
purge remains from test (cf. 5a53724fe247);
2019-07-28, by wenzelm
tuned;
2019-07-28, by wenzelm
clarified signature;
2019-07-28, by wenzelm
removed obsolete RC tags;
2019-07-28, by wenzelm
tuned;
2019-07-28, by wenzelm
clarified signature;
2019-07-28, by wenzelm
tuned;
2019-07-28, by wenzelm
tuned;
2019-07-27, by wenzelm
clarified signature;
2019-07-27, by wenzelm
tuned;
2019-07-27, by wenzelm
tuned;
2019-07-27, by wenzelm
tuned;
2019-07-27, by wenzelm
tuned -- reorder sections;
2019-07-26, by wenzelm
tuned;
2019-07-26, by wenzelm
proper argument type (amending 42fbb6abed5a);
2019-07-26, by wenzelm
tuned signature;
2019-07-26, by wenzelm
tuned;
2019-07-26, by wenzelm
finalize proofs earlier to reduce memory requirement;
2019-07-26, by wenzelm
proper proof_serial;
2019-07-26, by wenzelm
more explicit type proof_serial;
2019-07-26, by wenzelm
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
2019-07-26, by wenzelm
more accurate proof definitions (PThm nodes);
2019-07-25, by wenzelm
avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");
2019-07-24, by wenzelm
prefer local counter;
2019-07-24, by wenzelm
more accurate proof export;
2019-07-24, by wenzelm
clarified syntax;
2019-07-24, by wenzelm
tuned;
2019-07-24, by wenzelm
more thorough clean_proof;
2019-07-24, by wenzelm
clarified modules;
2019-07-24, by wenzelm
avoid global syntax for MinProof (amending e31271559de8);
2019-07-24, by wenzelm
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
2019-07-23, by wenzelm
discontinued Proofterm.Promise (cf. 725438ceae7c);
2019-07-23, by wenzelm
clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
2019-07-23, by wenzelm
tuned comments;
2019-07-23, by wenzelm
proof terms are always constructed sequentially;
2019-07-23, by wenzelm
tuned comments -- proper sections;
2019-07-22, by wenzelm
support export_proofs, prune_proofs;
2019-07-22, by wenzelm
clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
2019-07-22, by wenzelm
tuned;
2019-07-22, by wenzelm
clarified exception;
2019-07-22, by wenzelm
tuned;
2019-07-22, by wenzelm
more accurate type information;
2019-07-22, by wenzelm
unused (see also 42fbb6abed5a);
2019-07-22, by wenzelm
discontinued ASCII syntax;
2019-07-21, by wenzelm
global declaration of abstract syntax for proof terms, with qualified names;
2019-07-21, by wenzelm
tuned;
2019-07-21, by wenzelm
tuned;
2019-07-21, by wenzelm
more operations: support type classes within the logic;
2019-07-20, by wenzelm
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
2019-07-20, by wenzelm
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
2019-07-20, by wenzelm
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
2019-07-20, by wenzelm
More results about measure and integration theory
2019-07-19, by paulson
More analysis / measure theory material
2019-07-18, by paulson
merged
2019-07-18, by paulson
more new material about analysis
2019-07-18, by paulson
added forgotten declaration provided by Florian Haftmann
2019-07-18, by nipkow
merged;
2019-07-17, by wenzelm
updated to jedit_build-20190717: support more brackets;
2019-07-17, by wenzelm
updated to isabelle_fonts-20190717;
2019-07-17, by wenzelm
redundant;
2019-07-17, by wenzelm
tuned;
2019-07-17, by wenzelm
added \<llangle>, \<rrangle>;
2019-07-17, by wenzelm
tuned doc isar-ref;
2019-07-17, by wenzelm