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

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
added lemmas
2013-03-25, by nipkow
merged
2013-03-25, by wenzelm
clarified text_fold vs. fbrk;
2013-03-25, by wenzelm
tuned print_classes: more standard order, markup, formatting;
2013-03-25, by wenzelm
tuned message;
2013-03-25, by wenzelm
actually exit on scalac failure;
2013-03-25, by wenzelm
tuned signature;
2013-03-25, by wenzelm
removed obsolete uses of ext
2013-03-25, by kleing
prefer preset = 3 -- much faster and less memory requirement;
2013-03-24, by wenzelm
basic support for xz files;
2013-03-24, by wenzelm
added component xz-java-1.2;
2013-03-24, by wenzelm
more "quick start" hints;
2013-03-24, by wenzelm
simple case syntax for stream (stolen from AFP/Coinductive)
2013-03-24, by traytel
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
2013-03-23, by wenzelm
merged
2013-03-23, by wenzelm

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

isabelle