2015-06-12 haftmann 2015-06-12 standardized algebraic conventions: prefer a, b, c over x, y, z
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-11 paulson 2015-06-11 fixed several "inside-out" proofs
2015-06-11 hoelzl 2015-06-11 add transfer theorems for fixed points
2015-06-11 paulson 2015-06-11 Merge
2015-06-11 paulson 2015-06-11 tidied more proofs
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-06-10 wenzelm 2015-06-10 unused;
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-06-10 wenzelm 2015-06-10 more user aliases;
2015-06-10 wenzelm 2015-06-10 merged
2015-06-10 wenzelm 2015-06-10 prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;
2015-06-10 wenzelm 2015-06-10 tuned proofs;
2015-06-10 wenzelm 2015-06-10 clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';
2015-06-10 wenzelm 2015-06-10 support for "if prems" in local goal statements;
2015-06-10 wenzelm 2015-06-10 tuned message;
2015-06-10 wenzelm 2015-06-10 tuned proofs;
2015-06-10 wenzelm 2015-06-10 no need for protected goal (see 240ad53041c9);
2015-06-10 wenzelm 2015-06-10 tuned proofs;
2015-06-10 wenzelm 2015-06-10 prevent export of future result -- avoid interference with goal fixes;
2015-06-09 wenzelm 2015-06-09 more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-09 wenzelm 2015-06-09 allow for_fixes for 'have', 'show' etc.; tuned signature;
2015-06-09 wenzelm 2015-06-09 eliminated dead code;
2015-06-09 wenzelm 2015-06-09 clarified abstracted term bindings (again, see c8384ff11711);
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-09 wenzelm 2015-06-09 tuned;
2015-06-09 wenzelm 2015-06-09 clarified term bindings;
2015-06-10 fleury 2015-06-10 tuned
2015-06-10 Mathias Fleury 2015-06-10 Merge
2015-06-10 Mathias Fleury 2015-06-10 tuned
2015-06-10 Mathias Fleury 2015-06-10 Renaming multiset operators < ~> <#,...
2015-06-09 paulson 2015-06-09 more tidying up of proofs
2015-06-08 paulson 2015-06-08 tidying messy proofs
2015-06-08 paulson 2015-06-08 tidying messy proofs
2015-06-08 wenzelm 2015-06-08 merged
2015-06-08 wenzelm 2015-06-08 clarified context;
2015-06-08 wenzelm 2015-06-08 tuned;
2015-06-08 wenzelm 2015-06-08 clarified abstracted term bindings;
2015-06-08 wenzelm 2015-06-08 avoid duplicate warning due to Variable.warn_extra_tfrees;
2015-06-08 wenzelm 2015-06-08 clarified Proof_Context.cert_propp/read_propp; tuned;
2015-06-08 wenzelm 2015-06-08 more careful treatment of term bindings in 'obtain' proof body; tuned signature;
2015-06-08 wenzelm 2015-06-08 tuned signature;
2015-06-08 paulson 2015-06-08 Merge
2015-06-08 paulson 2015-06-08 Tidied lots of messy proofs
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned (see also 66e6c539a36d);
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 clarified: declare props once and for all; tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned;
2015-06-07 wenzelm 2015-06-07 tuned;
2015-06-07 wenzelm 2015-06-07 tuned;
2015-06-07 wenzelm 2015-06-07 tuned whitespace;
2015-06-06 wenzelm 2015-06-06 more tight treatment of subgoals: main goal may refer to extra variables;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';