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

Revise locale test theory layout.
2010-05-26, by ballarin
Merge mixins of distinct interpretations with same base.
2010-05-26, by ballarin
indicate prospective properties;
2010-05-27, by wenzelm
clarified auto_update vs. update;
2010-05-27, by wenzelm
more reactive message handling, notably for follow_caret mode;
2010-05-27, by wenzelm
Command.toString: include id for debugging;
2010-05-27, by wenzelm
merged
2010-05-26, by wenzelm
refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26, by wenzelm
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26, by boehmes
updated SMT certificates
2010-05-26, by boehmes
hide constants and types introduced by SMT,
2010-05-26, by boehmes
more convenient order of code equations
2010-05-26, by haftmann
misc updates for release;
2010-05-26, by wenzelm
eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-25, by wenzelm
moved ML files where they are actually used;
2010-05-25, by wenzelm
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
2010-05-25, by wenzelm
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-25, by wenzelm
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-25, by wenzelm
tuned -- avoid catch-all exception pattern;
2010-05-25, by wenzelm
updated generated files;
2010-05-25, by wenzelm
merged
2010-05-25, by wenzelm
merged
2010-05-24, by webertj
Typo fixed.
2010-05-24, by webertj
move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24, by huffman
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24, by huffman
move unused pattern match syntax stuff into HOLCF/ex
2010-05-24, by huffman
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-24, by huffman
more lemmas
2010-05-24, by haftmann
induction and case rules
2010-05-24, by haftmann
Store registrations in efficient data structure.
2010-05-24, by ballarin
Avoid recomputation of registration instance for lookup.
2010-05-24, by ballarin
Consistently use equality for registration lookup.
2010-05-24, by ballarin
Cleaner implementation of sublocale command.
2010-05-24, by ballarin
Reapply mixin patch: base for performance improvements.
2010-05-24, by ballarin
merged
2010-05-23, by huffman
declare a few more cont2cont rules
2010-05-23, by huffman
HOLCF no longer redefines 'consts' command
2010-05-22, by huffman
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
2010-05-22, by huffman
simplify fixrec continuity tactic
2010-05-22, by huffman
used sledgehammer[isar_proof] to replace slow metis call
2010-05-23, by krauss
Typo fixed.
2010-05-23, by webertj
Typo fixed.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
Improved document structure.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
merged
2010-05-23, by webertj
Refactoring, minor extensions (e.g., church_rosser).
2010-05-23, by webertj
NEWS: removed fixrec_simp attribute
2010-05-22, by huffman
merged
2010-05-22, by huffman
disambiguate some syntax
2010-05-22, by huffman
optimize continuity proofs in fixrec package, using cont2cont rules
2010-05-22, by huffman
add beta_cfun simproc, which uses cont2cont rules
2010-05-22, by huffman
removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-22, by huffman
simplify definition of eta_tac
2010-05-22, by huffman
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22, by huffman
remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-22, by huffman
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-22, by huffman
merged
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann

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

isabelle