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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
turned pattern unify flag into configuration option (global only);
2013-07-19, by wenzelm
merged
2013-07-19, by traytel
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
2013-07-19, by traytel
added exerciese
2013-07-19, by nipkow
do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
2013-07-19, by traytel
modify background theory where it is actually required (cf. 51dfdcd88e84);
2013-07-18, by wenzelm
tuned messages -- avoid text folds stemming from Pretty.chunks;
2013-07-18, by wenzelm
proper system options for 'find_theorems';
2013-07-18, by wenzelm
guard unify tracing via visible status of global theory;
2013-07-18, by wenzelm
provide global operations as well;
2013-07-18, by wenzelm
tuned signature;
2013-07-18, by wenzelm
tuned;
2013-07-18, by wenzelm
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-18, by wenzelm
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-18, by wenzelm
merged
2013-07-17, by wenzelm
tuned message;
2013-07-17, by wenzelm
tuned signature;
2013-07-17, by wenzelm
tuned
2013-07-17, by smolkas
merged
2013-07-17, by wenzelm
more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
2013-07-17, by wenzelm
tuned spelling;
2013-07-17, by wenzelm
show variants in error messages; more precise error messages (give witnesses for multiple instances)
2013-07-17, by Christian Sternagel
refactoring
2013-07-17, by Christian Sternagel
more robust exn_messages_ids;
2013-07-17, by wenzelm
non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
2013-07-17, by wenzelm
take context from static theory, not dynamic theory certificate;
2013-07-17, by wenzelm
more official Thm.eq_thm_strict, without demanding ML equality type;
2013-07-17, by wenzelm
tuned;
2013-07-17, by wenzelm
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
2013-07-17, by immler
merged
2013-07-16, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
tip