2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2013-03-29 wenzelm 2013-03-29 tuned message;
2013-03-29 haftmann 2013-03-29 convenience check for vain instantiation
2013-03-29 wenzelm 2013-03-29 improved centering via strikethrough offset;
2013-03-28 boehmes 2013-03-28 re-generated SMT certificates
2013-03-28 boehmes 2013-03-28 new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code
2013-03-28 wenzelm 2013-03-28 ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-28 kleing 2013-03-28 replace induction by hammer
2013-03-28 wenzelm 2013-03-28 merged
2013-03-28 wenzelm 2013-03-28 merged;
2013-03-28 wenzelm 2013-03-28 basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
2013-03-28 wenzelm 2013-03-28 maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;
2013-03-28 wenzelm 2013-03-28 tuned;
2013-03-28 wenzelm 2013-03-28 proper default browser info for interactive mode, notably thy_deps;
2013-03-28 nipkow 2013-03-28 improved pretty printing for state set acom
2013-03-27 ballarin 2013-03-27 Improvements to the print_dependencies command.
2013-03-27 wenzelm 2013-03-27 discontinued obsolete parallel_proofs_reuse_timing;
2013-03-27 wenzelm 2013-03-27 merged
2013-03-27 wenzelm 2013-03-27 separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
2013-03-27 wenzelm 2013-03-27 merged
2013-03-27 wenzelm 2013-03-27 extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27 wenzelm 2013-03-27 tuned;
2013-03-27 wenzelm 2013-03-27 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
2013-03-27 wenzelm 2013-03-27 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-03-27 wenzelm 2013-03-27 more liberal handling of skipped proofs;
2013-03-27 wenzelm 2013-03-27 explicit Toplevel.is_skipped_proof; tuned;
2013-03-27 wenzelm 2013-03-27 separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-27 wenzelm 2013-03-27 tuned;
2013-03-27 wenzelm 2013-03-27 tuned GUI;
2013-03-27 haftmann 2013-03-27 centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively
2013-03-26 haftmann 2013-03-26 avoid odd foundational terms after interpretation; more uniform code setup
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 wenzelm 2013-03-26 tuned session specification;
2013-03-26 wenzelm 2013-03-26 tuned proof;
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-26 wenzelm 2013-03-26 tuned proofs;
2013-03-26 haftmann 2013-03-26 explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 wenzelm 2013-03-26 proper input event handling;
2013-03-26 wenzelm 2013-03-26 more standard imports;
2013-03-26 wenzelm 2013-03-26 more specific Entry painting; ignore theories with all commands below threshold;
2013-03-26 wenzelm 2013-03-26 tuned;
2013-03-26 wenzelm 2013-03-26 mixed theory/command entries; tuned;
2013-03-26 wenzelm 2013-03-26 dockable window for timing information;
2013-03-26 kleing 2013-03-26 no \FIXME macro for ProgProve (moved to book)
2013-03-26 hoelzl 2013-03-26 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26 hoelzl 2013-03-26 rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26 hoelzl 2013-03-26 move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26 hoelzl 2013-03-26 move Ln.thy and Log.thy to Transcendental.thy
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 HOL-NSA should only import Complex_Main
2013-03-26 hoelzl 2013-03-26 rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26 hoelzl 2013-03-26 rename RealDef to Real
2013-03-26 hoelzl 2013-03-26 remove Real.thy
2013-03-26 hoelzl 2013-03-26 merge RComplete into RealDef