isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip

isabelle