isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

replace induction by hammer
2013-03-28, by kleing
merged
2013-03-28, by wenzelm
merged;
2013-03-28, by wenzelm
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, by wenzelm
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
2013-03-28, by wenzelm
tuned;
2013-03-28, by wenzelm
proper default browser info for interactive mode, notably thy_deps;
2013-03-28, by wenzelm
improved pretty printing for state set acom
2013-03-28, by nipkow
Improvements to the print_dependencies command.
2013-03-27, by ballarin
discontinued obsolete parallel_proofs_reuse_timing;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
2013-03-27, by wenzelm
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-03-27, by wenzelm
more liberal handling of skipped proofs;
2013-03-27, by wenzelm
explicit Toplevel.is_skipped_proof;
2013-03-27, by wenzelm
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27, by wenzelm
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, by wenzelm
clarified Skip_Proof.cheat_tac: more standard tactic;
2013-03-27, by wenzelm
tuned signature and module arrangement;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
tuned GUI;
2013-03-27, by wenzelm
centralized various multiset operations in theory multiset;
2013-03-27, by haftmann
avoid odd foundational terms after interpretation;
2013-03-26, by haftmann
more uniform style for interpretation and sublocale declarations
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
tuned session specification;
2013-03-26, by wenzelm
tuned proof;
2013-03-26, by wenzelm
tuned imports;
2013-03-26, by wenzelm
tuned proofs;
2013-03-26, by wenzelm
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
proper input event handling;
2013-03-26, by wenzelm
more standard imports;
2013-03-26, by wenzelm
more specific Entry painting;
2013-03-26, by wenzelm
tuned;
2013-03-26, by wenzelm
mixed theory/command entries;
2013-03-26, by wenzelm
dockable window for timing information;
2013-03-26, by wenzelm
no \FIXME macro for ProgProve (moved to book)
2013-03-26, by kleing
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26, by hoelzl
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26, by hoelzl
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, by hoelzl
Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26, by hoelzl
move Ln.thy and Log.thy to Transcendental.thy
2013-03-26, by hoelzl
move SEQ.thy and Lim.thy to Limits.thy
2013-03-26, by hoelzl
HOL-NSA should only import Complex_Main
2013-03-26, by hoelzl
rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26, by hoelzl
rename RealDef to Real
2013-03-26, by hoelzl
remove Real.thy
2013-03-26, by hoelzl
merge RComplete into RealDef
2013-03-26, by hoelzl
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26, by hoelzl
remove posreal_complete
2013-03-26, by hoelzl
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-26, by hoelzl
Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25, by ballarin
Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25, by ballarin
Fix issue related to mixins in roundup.
2013-03-25, by ballarin
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
2013-03-25, by kleing

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle