isabelle: Graph

merged
2019-09-23, by nipkow
Enforced precodition "n <= length xs" to avoid relying on "hd []".
2019-09-23, by nipkow
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
2019-09-23, by paulson
tuned
2019-09-23, by nipkow
added lemma
2019-09-23, by nipkow
proper file name instead of font name (amending dc9a39c3f75d);
2019-09-22, by wenzelm
added function
2019-09-22, by nipkow
merged
2019-09-19, by wenzelm
clarified data structures;
2019-09-19, by wenzelm
unused;
2019-09-19, by wenzelm
merged
2019-09-19, by paulson
Tidying and one more theorem
2019-09-19, by paulson
merged
2019-09-19, by wenzelm
explicit check of assumption prefix;
2019-09-19, by wenzelm
clarified signature;
2019-09-19, by wenzelm
clarified modules;
2019-09-19, by wenzelm
support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);
2019-09-18, by wenzelm
proper export of result_text for 'have';
2019-09-18, by wenzelm
support soft types for 'assume';
2019-09-18, by wenzelm
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
2019-09-18, by wenzelm
clarified modules;
2019-09-17, by wenzelm
clarified signature -- removed unused option (see acb0807ddb56);
2019-09-17, by wenzelm
one small last theorem
2019-09-19, by paulson
Four new results from Smooth_Manifolds/Analysis_More
2019-09-19, by paulson
A few more simple results
2019-09-19, by paulson
imported new material mostly due to Sébastien Gouëzel
2019-09-18, by paulson
A couple of new theorems, stolen from AFP entries
2019-09-17, by paulson
A few new theorems, tidying up and deletion of obsolete material
2019-09-17, by paulson
merged
2019-09-16, by wenzelm
more errors;
2019-09-16, by wenzelm
clarified inversion of file name to theory name, notably for Windows;
2019-09-16, by wenzelm
clarified import_name: observe directory notation more strictly;
2019-09-16, by wenzelm
tuned signature;
2019-09-16, by wenzelm
clarified signature -- removed pointless operations;
2019-09-16, by wenzelm
clarified signature -- removed unused content;
2019-09-16, by wenzelm
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
2019-09-16, by wenzelm
find theories via session directories only -- ignore known_theories;
2019-09-16, by wenzelm
tuned;
2019-09-16, by wenzelm
tuned message;
2019-09-16, by wenzelm
merged
2019-09-16, by nipkow
tuned
2019-09-16, by nipkow
A little-known material, and some tidying up
2019-09-16, by paulson
merged
2019-09-15, by wenzelm
tuned;
2019-09-15, by wenzelm
clarified theory status;
2019-09-15, by wenzelm
dump ZF in parallel to HOL Main;
2019-09-15, by wenzelm
tuned messages;
2019-09-15, by wenzelm
more ambitious options (again);
2019-09-15, by wenzelm
more ambitious options (again, after 93aa546ffbac);
2019-09-15, by wenzelm
tuned signature;
2019-09-15, by wenzelm
proper clean_theories wrt. dynamic dep_graph;
2019-09-15, by wenzelm
tuned signature;
2019-09-15, by wenzelm
potentially more robust: read under lock if not yet set;
2019-09-14, by wenzelm
tuned;
2019-09-13, by wenzelm
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
2019-09-13, by paulson
session directories need to exist;
2019-09-12, by wenzelm
clarified signature: eliminated unused option;
2019-09-12, by wenzelm
merged
2019-09-12, by paulson
importation fix
2019-09-12, by paulson
merged
2019-09-12, by paulson
new material on Analysis, plus some rearrangements
2019-09-12, by paulson
eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f);
2019-09-12, by wenzelm
discontinued obsolete "isabelle imports" and all_known data;
2019-09-12, by wenzelm
avoid duplicate directories wrt. synthetic session;
2019-09-12, by wenzelm
disallow accidental duplicates within the same session specification -- proper total match;
2019-09-12, by wenzelm
find theory files via session structure: much faster Prover IDE startup;
2019-09-12, by wenzelm
find theory node name via session directories;
2019-09-11, by wenzelm
disallow overlapping session directories;
2019-09-11, by wenzelm
tidied up some massive ugliness
2019-09-10, by paulson
clarified messages;
2019-09-08, by wenzelm
clarified syntax: 'directories' and 'theories' belong together;
2019-09-08, by wenzelm
more documentation;
2019-09-08, by wenzelm
check session directories;
2019-09-08, by wenzelm
declare session directories;
2019-09-08, by wenzelm
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
2019-09-08, by wenzelm
theory_name based on session_directories: no need for expensive all_known;
2019-09-07, by wenzelm
clarified session_directories: relative to session_path, with overlapping information;
2019-09-07, by wenzelm
clarified signature: retain global session information, unaffected by later restriction;
2019-09-07, by wenzelm
disable fragile options for now;
2019-09-07, by wenzelm
avoid overlapping session directories;
2019-09-07, by wenzelm
support for explicit session directories;
2019-09-07, by wenzelm
obsolete (see 94442fce40a5);
2019-09-06, by wenzelm
optional trace output;
2019-09-06, by wenzelm
prefer commands_accepted: fewer protocol messages;
2019-09-06, by wenzelm
prefer define_commands_bulk: fewer protocol messages;
2019-09-06, by wenzelm
clarified signature;
2019-09-06, by wenzelm
tuned signature -- prefer bulk messages;
2019-09-06, by wenzelm
tuned signature;
2019-09-06, by wenzelm
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
2019-09-06, by wenzelm
more robust;
2019-09-06, by wenzelm
unused;
2019-09-06, by wenzelm
proper finished_theory status for result;
2019-09-06, by wenzelm
more central checkpoint;
2019-09-06, by wenzelm
disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;
2019-09-04, by wenzelm
merged
2019-09-04, by wenzelm
load theories in stages, to reduce ML heap requirements;
2019-09-04, by wenzelm
more complete graph;
2019-09-04, by wenzelm
tuned messages;
2019-09-04, by wenzelm
tuned signature;
2019-09-04, by wenzelm
clarified signature;
2019-09-03, by wenzelm
tuned important special case;
2019-09-03, by wenzelm
tuned signature;
2019-09-03, by wenzelm
more dump_checkpoints;
2019-09-03, by wenzelm
clarified signature;
2019-09-03, by wenzelm
clarified state variable: avoid extra mutability via Promise;
2019-09-03, by wenzelm
Removal of the redundant ancestor Continuous_Extension
2019-09-04, by paulson
Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
2019-09-04, by paulson
Theory Derivative no longer depends on Path_Connected
2019-09-04, by paulson
more explicit type Dump.Session, with context information;
2019-09-02, by wenzelm
proper orientation;
2019-09-02, by wenzelm
clarified signature: prefer operations without position;
2019-09-02, by wenzelm
prefer Theory_Ordering theory names are unique (due to proper session context);
2019-09-02, by wenzelm
clarified signature: full dependency graph;
2019-09-01, by wenzelm
merged
2019-08-31, by wenzelm
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
2019-08-29, by wenzelm
tuned signature;
2019-08-29, by wenzelm
merged
2019-08-29, by nipkow
simplified proofs
2019-08-29, by nipkow
more rules for ordered real vector spaces
2019-08-29, by haftmann
simplified setup
2019-08-29, by nipkow
tuned proof
2019-08-29, by nipkow
merged
2019-08-28, by wenzelm
enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;
2019-08-28, by wenzelm
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
2019-08-28, by wenzelm
more scalable -- less ML heap requirements;
2019-08-28, by wenzelm
tuned whitespace;
2019-08-28, by wenzelm
Integrate locale activation fallback diagnostics with 'trace_locales'.
2019-08-28, by ballarin
entry point for analysis without integration theory
2019-08-28, by immler
removed Brouwer_Fixpoint from imports of Derivative
2019-08-28, by immler
removed unused lemma, generalized, reduced dependencies
2019-08-27, by immler
fixed typo
2019-08-27, by immler
moved lemmas; reduced dependencies of Lipschitz
2019-08-27, by immler
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
2019-08-27, by immler
merged
2019-08-27, by nipkow
moved lemmas
2019-08-27, by nipkow
moved basic theorem
2019-08-27, by immler
proper positions for 'termination' command (see also 5549e686d6ac);
2019-08-27, by wenzelm
tuned names -- proper scopes;
2019-08-27, by wenzelm
added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);
2019-08-26, by wenzelm
proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;
2019-08-25, by wenzelm
Tracing of locale activation.
2019-08-24, by ballarin
tuned
2019-08-23, by nipkow
always export Pure proofs;
2019-08-23, by wenzelm
clarified 'thm_deps' command;
2019-08-23, by wenzelm
more compact: avoid pointless PThm rudiments;
2019-08-23, by wenzelm
clarified signature: prefer total operations;
2019-08-23, by wenzelm
proper graph traversal: avoid multiple visit of unnamed nodes;
2019-08-21, by wenzelm
more scalable: avoid huge intermediate XML elems;
2019-08-21, by wenzelm
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
2019-08-21, by wenzelm
NEWS;
2019-08-20, by wenzelm
merged
2019-08-20, by wenzelm
export thm_deps;
2019-08-20, by wenzelm
proper theory context;
2019-08-20, by wenzelm
clarified thm_id vs. thm_node/thm: retain theory_name;
2019-08-20, by wenzelm
clarified signature;
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
unused (see 095dadc62bb5);
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
tuned signature;
2019-08-20, by wenzelm
clarified modules;
2019-08-20, by wenzelm
clarified modules;
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
clarified signature;
2019-08-20, by wenzelm
tuned
2019-08-20, by nipkow
tuned
2019-08-20, by nipkow
merged
2019-08-20, by nipkow
tuned
2019-08-20, by nipkow
merged
2019-08-19, by wenzelm
clarified signature;
2019-08-19, by wenzelm
clarified export of axioms and theorems (identified derivations instead of projected facts);
2019-08-19, by wenzelm
tuned signature;
2019-08-19, by wenzelm
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
2019-08-19, by wenzelm
module Thm_Name for Isabelle/Scala;
2019-08-19, by wenzelm
tuned;
2019-08-19, by wenzelm
clarified modules;
2019-08-19, by wenzelm
tuned;
2019-08-19, by wenzelm
tuned
2019-08-19, by nipkow
tuned names
2019-08-19, by nipkow
clarified signature;
2019-08-17, by wenzelm
discontinued peek_status: unused and not clearly defined;
2019-08-17, by wenzelm
more documentation on oracles;
2019-08-17, by wenzelm
proper theory context for global props;
2019-08-17, by wenzelm
more thorough check, using full dependency graph of finished proofs;
2019-08-17, by wenzelm
added ML antiquotation @{oracle_name};
2019-08-17, by wenzelm
more robust, notably for open_proof of unnamed derivation;
2019-08-17, by wenzelm
tuned comments;
2019-08-17, by wenzelm
NEWS;
2019-08-17, by wenzelm
more accurate proposition for cheat_tac (command 'sorry');
2019-08-17, by wenzelm
added command 'thm_oracles';
2019-08-17, by wenzelm
clarified type for recorded oracles;
2019-08-17, by wenzelm
unused;
2019-08-17, by wenzelm
clarified signature;
2019-08-17, by wenzelm
clarified modules;
2019-08-17, by wenzelm
clarified lookup operations: more scalable for multiple retrieval;
2019-08-17, by wenzelm
clarified signature;
2019-08-17, by wenzelm
merged
2019-08-16, by wenzelm
maintain thm_name vs. derivation_id for global facts;
2019-08-16, by wenzelm
clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;
2019-08-16, by wenzelm
clarified signature;
2019-08-16, by wenzelm
Fixed brace matching (plus some whitespace cleanup)
2019-08-16, by paulson
merged
2019-08-16, by paulson
new material on eqiintegrable functions, etc.
2019-08-16, by paulson
clarified treatment of individual theorems;
2019-08-16, by wenzelm
tuned signature;
2019-08-16, by wenzelm
clarified signature;
2019-08-16, by wenzelm
clarified derivation_name vs. raw_derivation_name;
2019-08-16, by wenzelm
merged
2019-08-15, by wenzelm
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
2019-08-15, by wenzelm
more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
2019-08-15, by wenzelm
support Export_Theory.read_proof, based on theory_name and serial;
2019-08-15, by wenzelm
clarified PThm: theory_name simplifies retrieval from exports;
2019-08-15, by wenzelm
Indexname.toString according to string_of_vname' in ML;
2019-08-15, by wenzelm
clarified type Indexname, with plain value Int;
2019-08-15, by wenzelm
more complete pattern match;
2019-08-15, by wenzelm
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
2019-08-15, by wenzelm
support for (fully reconstructed) proof terms in Scala;
2019-08-15, by wenzelm
new material; rotated premises of Lim_transform_eventually
2019-08-15, by paulson
clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
2019-08-14, by wenzelm
tuned;
2019-08-14, by wenzelm
uniform standard_vars for terms and proof terms;
2019-08-14, by wenzelm
treat simproc results as atomic -- more compact proof terms;
2019-08-14, by wenzelm
tuned;
2019-08-13, by wenzelm
minor performance tuning;
2019-08-13, by wenzelm
NEWS and example for Theory.join_theory;
2019-08-13, by wenzelm
tuned whitespace;
2019-08-13, by wenzelm
more compact proof terms;
2019-08-13, by wenzelm
more documentation;
2019-08-13, by wenzelm
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
2019-08-13, by wenzelm
clarified modules;
2019-08-13, by wenzelm
merged
2019-08-12, by wenzelm
more compact proof terms;
2019-08-12, by wenzelm
more robust -- notably for metis, which tends to accumulate tpairs;
2019-08-12, by wenzelm
tuned -- avoid shadowing of ML names;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
more compact proof terms;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
tuned -- eliminated unused parameters;
2019-08-12, by wenzelm
more direct/compact export of proof terms;
2019-08-12, by wenzelm
output physical_stderr, e.g. for low-level debugging;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
do not open ML structures;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
misc tuning -- slightly more readable;
2019-08-12, by wenzelm
simplified defs (thanks to Mohammad)
2019-08-12, by nipkow
record sort constraints unconditionally: minimal performance implications;
2019-08-11, by wenzelm
more careful export of unnamed proof boxes: avoid duplicates via memoing;
2019-08-10, by wenzelm
tuned signature;
2019-08-10, by wenzelm
export each PThm node separately: slightly more scalable;
2019-08-10, by wenzelm
allow duplicate exports via strict = false;
2019-08-10, by wenzelm
tuned message;
2019-08-10, by wenzelm
more positions;
2019-08-10, by wenzelm
more positions;
2019-08-10, by wenzelm
tuned;
2019-08-09, by wenzelm
formal position for PThm nodes;
2019-08-09, by wenzelm
clarified ML types;
2019-08-09, by wenzelm
proper treatment of body oracles, outside of recursion into thms graph;
2019-08-09, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-08, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-08, by wenzelm
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
added \<bbar>;
2019-07-17, by wenzelm
added \<sqdot>;
2019-07-17, by wenzelm
fixed renaming issues
2019-07-17, by paulson
merged
2019-07-17, by paulson
a few new lemmas and a bit of tidying
2019-07-17, by paulson
support for a soft-type system within the Isabelle logical framework;
2019-07-16, by wenzelm
tuned
2019-07-11, by nipkow
proper theory naming after join (reset due to merge_data);
2019-07-04, by wenzelm
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
2019-07-04, by wenzelm
clarified history stage: allow independent updates that are merged later;
2019-07-04, by wenzelm
support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
2019-06-24, by wenzelm
proper quasi-total merge
2019-06-23, by haftmann
made LaTeX happy
2019-06-22, by haftmann
streamlined setup for linear algebra, particularly removed redundant rule declarations
2019-06-22, by haftmann
tuned
2019-06-22, by haftmann
tuned
2019-06-21, by haftmann
even more appropriate fact name
2019-06-16, by haftmann
more correct indicator
2019-06-16, by haftmann
make latex happy
2019-06-14, by haftmann
moved some theorems into HOL main corpus
2019-06-14, by haftmann
misc tuning and modernization
2019-06-14, by haftmann
more theorems for proof of concept for word type
2019-06-14, by haftmann
official fact collection sign_simps
2019-06-14, by haftmann
tuned proofs
2019-06-14, by haftmann
avoid pseudo-collection to be used in generated proofs
2019-06-14, by haftmann
moved comment to approproiate place
2019-06-14, by haftmann
removed outcommented example which seems not to work as advertized
2019-06-14, by haftmann
clear separation of types for bits (False / True) and Z2 (0 / 1)
2019-06-14, by haftmann
generalized type classes for parity to cover word types also, which contain zero divisors
2019-06-14, by haftmann
slightly more specialized name for type class
2019-06-14, by haftmann
dropped weaker legacy alias
2019-06-14, by haftmann
slightly more stringent ordering of theorems
2019-06-14, by haftmann
removed relics of ASCII syntax for indexed big operators
2019-06-14, by haftmann
dropped former legacy input abbreviations
2019-06-14, by haftmann
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
2019-06-14, by haftmann
prefer fixed simpset for proof procedure
2019-06-14, by haftmann
tuned file system structure
2019-06-14, by haftmann
avoid spammed sledgehammer proofs
2019-06-14, by haftmann
added lemmas
2019-06-11, by nipkow
proper URL;
2019-06-09, by wenzelm
merged;
2019-06-09, by wenzelm
Added tag Isabelle2019 for changeset 83774d669b51
2019-06-09, by wenzelm
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
2019-06-07, by blanchet
tuned;
2019-06-04, by wenzelm
tuned;
2019-06-04, by wenzelm
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
2019-06-04, by wenzelm
unused;
2019-06-04, by wenzelm
tuned messages;
2019-06-04, by wenzelm
proper context;
2019-06-04, by wenzelm
misc tuning and clarification, notably wrt. flow of context;
2019-06-04, by wenzelm
proper context;
2019-06-04, by wenzelm
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
2019-06-04, by wenzelm
unused;
2019-06-04, by wenzelm
misc tuning and clarification, notably wrt. flow of context;
2019-06-04, by wenzelm
proper context;
2019-06-04, by wenzelm
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
2019-06-04, by wenzelm
more structural integrity;
2019-06-03, by wenzelm
tuned;
2019-06-03, by wenzelm
more structural integrity;
2019-06-03, by wenzelm
clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
2019-06-03, by wenzelm
tuned;
2019-06-03, by wenzelm
clarified signature;
2019-06-03, by wenzelm
tuned whitespace;
2019-06-03, by wenzelm
clarified context: prefer abstract Variable.auto_fixes;
2019-06-03, by wenzelm
tuned;
2019-06-03, by wenzelm
tuned signature;
2019-06-03, by wenzelm
redundant: default is false;
2019-06-03, by wenzelm
tuned imports -- accommodate scala-2.13.0-RC3;
2019-06-01, by wenzelm
tuned -- accommodate scala-2.13.0-RC3;
2019-06-01, by wenzelm
merged
2019-06-01, by wenzelm
Added tag Isabelle2019-RC4 for changeset ad2d84c42380 Isabelle2019
2019-06-01, by wenzelm
hint on printing via Web browser;
2019-06-01, by wenzelm
tuned;
2019-05-28, by wenzelm
tuned proof
2019-05-31, by nipkow
tuned
2019-05-31, by nipkow
merged
2019-05-27, by wenzelm
more direct invocation of Windows exe: avoid extra bash, cygpath, exec;
2019-05-27, by wenzelm
tuned whitespace;
2019-05-27, by wenzelm
updated to bash_process-1.2.3: rebuild on current reference PLATFORMS;
2019-05-27, by wenzelm
Added tag Isabelle2019-RC3 for changeset 85de4fdec61b
2019-05-25, by wenzelm
more robust InstallPath (amending 4ce07be8ba17): self-directory may be odd temp dir produced by browser "Run" operation;
2019-05-24, by wenzelm
avoid extra subprocess -- potentially more robust on Cygwin;
2019-05-24, by wenzelm
updated to cygwin-20190524;
2019-05-24, by wenzelm
proper version;
2019-05-21, by wenzelm
tuned spelling;
2019-05-19, by wenzelm
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
2019-05-19, by wenzelm
tuned whitespace;
2019-05-19, by wenzelm
tuned signature (following Scala version);
2019-05-18, by wenzelm
tuned;
2019-05-18, by wenzelm
obsolete (incompatible with Isabelle2019);
2019-05-14, by wenzelm
amended to unoverload actually all parameters of a type variable
2019-05-13, by immler
proper message;
2019-05-13, by wenzelm
Finite_Map: move lemmas from LambdaAuth AFP entry
2019-05-22, by Lars Hupel
documentation for termination_simp attribute
2019-05-21, by krauss
strengthened lemma
2019-05-21, by nipkow
tuned names
2019-05-20, by nipkow
tuned name
2019-05-16, by nipkow
tuned
2019-05-16, by nipkow
a few general lemmas
2019-05-15, by paulson
Generalisations involving numerals; comparisons should now work for ennreal
2019-05-15, by paulson
tuned
2019-05-14, by nipkow