isabelle: Graph

merged
2010-02-02, by berghofe
merged
2010-01-31, by berghofe
Adapted to changes in cases method.
2010-01-30, by berghofe
Adapted to changes in setup of cases method.
2010-01-30, by berghofe
Added setup for simplification of equality constraints in cases rules.
2010-01-30, by berghofe
Added infrastructure for simplifying equality constraints in cases rules.
2010-01-30, by berghofe
Added "constraints" tag / attribute for specifying the number of equality
2010-01-30, by berghofe
updated SMT certificates
2010-02-02, by boehmes
updated SMT examples
2010-02-02, by boehmes
collect certificates in a single file
2010-02-02, by boehmes
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-02-02, by blanchet
Removed explicit type annotations
2010-02-01, by himmelma
adjusted to changes in List_Set.thy
2010-01-31, by haftmann
more correspondence lemmas between related operations
2010-01-31, by haftmann
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
dropped some redundancies
2010-01-31, by haftmann
generalized lemma foldl_apply_inv to foldl_apply
2010-01-31, by haftmann
more correspondence lemmas between related operations; tuned some proofs
2010-01-31, by haftmann
new theory Algebras.thy for generic algebraic structures
2010-01-28, by haftmann
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-28, by haftmann
merged
2010-01-27, by haftmann
a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
2010-01-27, by haftmann
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
same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-10, by berghofe
Tuned some proofs; nicer case names for some of the induction / cases rules.
2010-01-10, by berghofe
Added setup for simplification of equality constraints in induction rules.
2010-01-10, by berghofe
Added infrastructure for simplifying equality constraints.
2010-01-10, by berghofe
spurious proof failure
2010-01-15, by haftmann
merged
2010-01-14, by haftmann
merged
2010-01-14, by haftmann
dropped unused binding
2010-01-14, by haftmann
dedicated conversions to and from Int
2010-01-14, by haftmann
printing of cases
2010-01-14, by haftmann
tuned for products vs. tupled functions
2010-01-14, by haftmann
added Scala setup
2010-01-14, by haftmann
allow individual printing of numerals during code serialization
2010-01-14, by haftmann
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2010-01-14, by blanchet
adjusted to changes in code equation administration
2010-01-14, by haftmann
explicit abstract type of code certificates
2010-01-13, by haftmann
corrected error messages; tuned
2010-01-13, by haftmann
function transformer preprocessor applies to both code generators
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
code certificates as integral part of code generation
2010-01-12, by haftmann
import of antiquote_setup not necessary
2010-01-13, by haftmann
merged
2010-01-13, by haftmann
being more accurate wrt. list syntax
2010-01-13, by haftmann
deactivate pretty code test for Scala -- no proper setup yet
2010-01-13, by haftmann
some syntax setup for Scala
2010-01-13, by haftmann
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2010-01-13, by wenzelm
merged
2010-01-12, by wenzelm
Parsing errors during proof reconstruction now give rise to an intelligible error message.
2010-01-12, by paulson
rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
2010-01-12, by wenzelm
tuned initial properties/perspective;
2010-01-12, by wenzelm
provide JEDIT_SETTINGS via settings;
2010-01-12, by wenzelm
updated version and dependencies;
2010-01-12, by wenzelm
recovered subscript (cf. ded5b770ec1c);
2010-01-12, by wenzelm
formal antiquotations for ML snippets; no "open" unsynchronized references
2010-01-12, by haftmann
clarified terminology;
2010-01-11, by wenzelm
merged
2010-01-11, by wenzelm
added code certificates
2010-01-11, by haftmann
tuned code equations
2010-01-11, by haftmann