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 -60 +60 +100 +300 +1000 +3000 +10000 tip

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

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

isabelle