Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)
Summary
- fixed by simp add: greaterThan_0
- replaced or repaired proofs (by simp add: Complex_eq)
The file was modified | thys/Ergodic_Theory/Invariants.thy |
The file was modified | thys/Ergodic_Theory/Recurrence.thy |
The file was modified | thys/Polynomial_Interpolation/Is_Rat_To_Rat.thy |
Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- tuned;
- proper columns;
- tuned signature;
- more general signature: not limited to SQLite;
- suppress inlined properties from log output;
- prefer database, but also accept log.gz from historic versions;
- more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;
- maintain persistent session info in SQLite database instead of log file;
- tuned;
- tuned signature;
- tuned;
- tuned message;
- clarified signature;
- more selective queries;
- clarified data representation;
- data representation with XML.Cache; tuned;
- clarified name;
- SQL database operations for combined session info;
- prefer non-strict default;
- clarified signature (again, see also 3ed43cfc8b14);
- tuned signature;
- tuned;
- tuned comments;
- clarified message: exception output usally happens in a context without extra newline;