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

lemma Image_closed_trancl
2010-01-27, by haftmann
corrected type of typecopy constructor
2010-01-27, by haftmann
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
2010-01-27, by haftmann
Changed author; removed debugging code.
2010-01-27, by berghofe
merged
2010-01-25, by bulwahn
adding Mutabelle to repository
2010-01-25, by bulwahn
Replaced vec1 and dest_vec1 by abbreviation.
2010-01-25, by hoelzl
merged
2010-01-22, by haftmann
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22, by haftmann
merged
2010-01-22, by boehmes
support skolem constant for extensional arrays in Z3 proofs
2010-01-22, by boehmes
drop underscores at end of names coming from Boogie
2010-01-22, by boehmes
merged
2010-01-22, by bulwahn
correctly hiding facts of Lazy_Sequence
2010-01-22, by bulwahn
corrected and simplified Spec_Rules registration in the Recdef package
2010-01-21, by bulwahn
merged
2010-01-21, by bulwahn
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
2010-01-21, by bulwahn
adopting Sequences
2010-01-20, by bulwahn
added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2010-01-20, by bulwahn
merged
2010-01-20, by bulwahn
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-18, by krauss
merged
2010-01-20, by bulwahn
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-20, by bulwahn
simplified proofs
2010-01-22, by haftmann
NEWS
2010-01-22, by haftmann
more accurate dependencies
2010-01-22, by haftmann
code literals: distinguish numeral classes by different entries
2010-01-22, by haftmann
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
2010-01-22, by haftmann
merged
2010-01-21, by haftmann
dropped some old primrecs and some constdefs
2010-01-16, by haftmann
explicit CONST in translations
2010-01-16, by haftmann
modernized syntax
2010-01-16, by haftmann
fix issues with previous Nitpick change
2010-01-20, by blanchet
merged
2010-01-20, by blanchet
some work on Nitpick's support for quotient types;
2010-01-20, by blanchet
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
2010-01-14, by blanchet
Added transpose_rectangle, when the input list is rectangular.
2010-01-19, by hoelzl
Add transpose to the List-theory.
2010-01-19, by hoelzl
some examples for basic context operations;
2010-02-02, by wenzelm
minimal tuning of this slightly dated material;
2010-02-02, by wenzelm
added Subgoal.FOCUS;
2010-02-02, by wenzelm
misc tuning and clarification;
2010-02-02, by wenzelm
moved examples to proper place;
2010-02-02, by wenzelm
more details on long names, binding/naming, name space;
2010-02-01, by wenzelm
Variable.names_of;
2010-01-31, by wenzelm
more details on Isabelle symbols;
2010-01-31, by wenzelm
theory data example;
2010-01-29, by wenzelm
basic setup for ML examples: tag "mlex";
2010-01-29, by wenzelm
tuned signature;
2010-01-28, by wenzelm
formal markup of type aliases;
2010-01-28, by wenzelm
make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
2010-01-28, by wenzelm
Netbeans Library "Scala-compiler";
2010-01-16, by wenzelm
union is an abbreviation for sup.
2010-01-15, by berghofe
merged
2010-01-15, by berghofe
Eliminated is_open option of Rule_Cases.make_nested/make_common;
2010-01-15, by berghofe
Adapted to changes in induct method.
2010-01-10, by berghofe
Adapted to changes in setup of induct method.
2010-01-10, by berghofe
Expand proofs of induct_atomize'/rulify'.
2010-01-10, by berghofe
Changed case names of converse_rtranclp_induct.
2010-01-10, by berghofe
Injectivity / distinctness theorems are now used to simplify induction rules.
2010-01-10, by berghofe

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

isabelle