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
2015-06-10, by Mathias Fleury
Renaming multiset operators < ~> <#,...
2015-06-10, by Mathias Fleury
more tidying up of proofs
2015-06-09, by paulson
tidying messy proofs
2015-06-08, by paulson
tidying messy proofs
2015-06-08, by paulson
merged
2015-06-08, by wenzelm
clarified context;
2015-06-08, by wenzelm
tuned;
2015-06-08, by wenzelm
clarified abstracted term bindings;
2015-06-08, by wenzelm
avoid duplicate warning due to Variable.warn_extra_tfrees;
2015-06-08, by wenzelm
clarified Proof_Context.cert_propp/read_propp;
2015-06-08, by wenzelm
more careful treatment of term bindings in 'obtain' proof body;
2015-06-08, by wenzelm
tuned signature;
2015-06-08, by wenzelm
Merge
2015-06-08, by paulson
Tidied lots of messy proofs
2015-06-08, by paulson
tuned signature;
2015-06-07, by wenzelm
tuned (see also 66e6c539a36d);
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
clarified: declare props once and for all;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned whitespace;
2015-06-07, by wenzelm
more tight treatment of subgoals: main goal may refer to extra variables;
2015-06-06, by wenzelm
added Isar command 'supply';
2015-06-05, by wenzelm
tuned;
2015-06-05, by wenzelm
clarified signature -- better support for Isar commands outside of Pure;
2015-06-05, by wenzelm
merged
2015-06-03, by wenzelm
clarified context;
2015-06-03, by wenzelm
tuned;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
cleaified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
tuned proof;
2015-06-02, by wenzelm
merged
2015-06-03, by noschinl
simps_of_case: Better error if split rule is not an equality
2015-06-02, by noschinl
simps_of_case: allow Drule.dummy_thm as ignored split rule
2015-06-02, by noschinl
implicit partial divison operation in integral domains
2015-06-01, by haftmann
separate class for division operator, with particular syntax added in more specific classes
2015-06-01, by haftmann
explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
2015-06-01, by haftmann
dropped dead config option
2015-06-01, by haftmann
tuned, including proper signature for functor argument
2015-06-01, by haftmann
dropped dead code
2015-06-01, by haftmann
explicit argument expansion of uncheck rules;
2015-06-01, by haftmann
explicit input marker for operations
2015-06-01, by haftmann
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
2015-06-01, by haftmann
self-contained formulation of abbrev for named targets
2015-06-01, by haftmann
correct sort constraints for abbreviations in type classes
2015-06-01, by haftmann
separate function to compute exported abbreviation
2015-06-01, by haftmann
clearly separated target primitives (target_foo) from self-contained target operations (foo)
2015-06-01, by haftmann
tuned order
2015-06-01, by haftmann
dedicated config options to deactivate uncheck phase for improvable syntax
2015-06-01, by haftmann
clarified interfaces for improvable syntax
2015-06-01, by haftmann
tuned
2015-06-01, by haftmann
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
2015-06-01, by wenzelm
discontinued legacy;
2015-06-01, by wenzelm
obsolete (see 189c81779a68);
2015-06-01, by wenzelm
eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
obsolete;
2015-05-31, by wenzelm
clarified context;
2015-05-31, by wenzelm
tuned;
2015-05-31, by wenzelm
tuned;
2015-05-31, by wenzelm
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30, by wenzelm
tuned spelling;
2015-05-30, by wenzelm
unused;
2015-05-30, by wenzelm
tuned;
2015-05-30, by wenzelm
more explicit context;
2015-05-30, by wenzelm
obsolete;
2015-05-30, by wenzelm
tuned -- more direct Thm.renamed_prop;
2015-05-30, by wenzelm
tuned message;
2015-05-30, by wenzelm
tuned whitespace;
2015-05-30, by wenzelm
removed model checks from Nitpick
2015-05-29, by blanchet
document Nitpick issue
2015-05-29, by blanchet
uncountability: open interval equivalences
2015-05-29, by paulson
Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-28, by paulson
made Auto Sledgehammer behave more like the real thing
2015-05-28, by blanchet
took out Sledgehammer minimizer optimization that breaks things
2015-05-28, by blanchet
modernized (slightly) type compiler in MicroJava
2015-05-28, by kleing
New material about paths, and some lemmas
2015-05-26, by paulson
removed obsolete RC tags;
2015-05-25, by wenzelm
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-25, by wenzelm
Added tag Isabelle2015 for changeset 5ae2a2e74c93
2015-05-25, by wenzelm
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature; Isabelle2015
2015-05-23, by wenzelm
updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;
2015-05-22, by wenzelm
tuned;
2015-05-22, by wenzelm
tuned;
2015-05-22, by wenzelm
updated versions;
2015-05-21, by wenzelm
tuned;
2015-05-21, by wenzelm
tuned;
2015-05-21, by wenzelm
cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;
2015-05-20, by wenzelm
more on displays with very high resolution;
2015-05-19, by wenzelm
add Haskabelle-2015 component
2015-05-18, by Lars Noschinski
Added tag Isabelle2015-RC5 for changeset d7f636331176
2015-05-17, by wenzelm
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
2015-05-17, by wenzelm
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
2015-05-17, by wenzelm
tuned;
2015-05-17, by wenzelm
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
2015-05-16, by wenzelm
clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
2015-05-13, by wenzelm
tuned whitespace;
2015-05-13, by wenzelm
more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;
2015-05-13, by wenzelm
Added tag Isabelle2015-RC4 for changeset 05fe9bdc4f8f
2015-05-09, by wenzelm
new CVC4 component
2015-05-09, by blanchet
took out unreliable 'blast' from tactic altogether
2015-05-09, by blanchet