Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)
Summary
- Patched some failing proofs
- transfer of a few results to the main Analysis library
The file was modified | thys/Smooth_Manifolds/Smooth.thy |
The file was modified | thys/Gromov_Hyperbolicity/Library_Complements.thy |
The file was modified | thys/Smooth_Manifolds/Analysis_More.thy |
Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- clarified data structures; eliminated presumably obsolete check of known_theories: should be unique by construction;
- unused;
- merged
- Tidying and one more theorem
- merged
- explicit check of assumption prefix;
- clarified signature;
- clarified modules;
- support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);
- proper export of result_text for 'have';
- support soft types for 'assume'; clarified "text": avoid polymorphism due to premature export;
- more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
- clarified modules;
- clarified signature -- removed unused option (see acb0807ddb56);
- one small last theorem
- Four new results from Smooth_Manifolds/Analysis_More
- A few more simple results