isabelle: Graph

modernized syntax translations, using mostly abbreviation/notation;
2010-02-10, by wenzelm
simple proofs make life faster and easier
2010-02-09, by haftmann
merged
2010-02-09, by haftmann
hide fact names clashing with fact names from Group.thy
2010-02-09, by haftmann
dropped lemma duplicates
2010-02-09, by haftmann
isatest: activated HOL-Nitpick_Examples (by adding component kodkodi) on some platforms where it mostly works as expected;
2010-02-09, by wenzelm
adjusted to cs. 9f841f20dca6
2010-02-09, by haftmann
merged
2010-02-08, by huffman
correct definedness side conditions for copy_apps and take_apps
2010-02-08, by huffman
handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
2010-02-08, by huffman
rewrite proof script for take_stricts
2010-02-07, by huffman
remove redundant theorem attributes
2010-02-07, by huffman
add lemma iterate_below_fix
2010-02-07, by huffman
modernized some syntax translations;
2010-02-08, by wenzelm
more precise dependencies;
2010-02-08, by wenzelm
merged
2010-02-08, by haftmann
re-generated certificates
2010-02-08, by haftmann
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08, by haftmann
tuned spelling
2010-02-08, by haftmann
tuned proofs
2010-02-08, by haftmann
hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-02-08, by haftmann
tuned header
2010-02-08, by haftmann
using code antiquotation
2010-02-08, by haftmann
tuned header
2010-02-08, by haftmann
dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08, by haftmann
NEWS: ax_simps
2010-02-08, by haftmann
avoid upto in generated code (is infix operator in library.ML)
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
2010-02-08, by haftmann
merged
2010-02-08, by haftmann
more precise proofs
2010-02-08, by haftmann
moved auxiliary lemmas to more appropriate places
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
2010-02-08, by haftmann
dropped instantiations for combined lattices
2010-02-08, by haftmann
added lemmas involving Min, Max, uminus
2010-02-08, by haftmann
tuned proof
2010-02-08, by haftmann
separate library theory for type classes combining lattices with various algebraic structures
2010-02-08, by haftmann
more quotes;
2010-02-08, by wenzelm
merged
2010-02-08, by haftmann
separate theory for index structures
2010-02-08, by haftmann
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05, by haftmann
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05, by haftmann
added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration
2010-02-05, by haftmann
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
2010-02-08, by boehmes
removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);
2010-02-07, by wenzelm
modernized perl scripts: prefer standalone executables;
2010-02-07, by wenzelm
modernized perl scripts: prefer standalone executables;
2010-02-07, by wenzelm
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-07, by wenzelm
prefer explicit @{lemma} over adhoc forward reasoning;
2010-02-07, by wenzelm
simplified interface for ML antiquotations, struct_name is always "Isabelle";
2010-02-07, by wenzelm
tuned isatest ML_OPTIONS;
2010-02-06, by wenzelm
removed ever experimental support for Moscow ML -- hardly works anymore;
2010-02-06, by wenzelm
result: Single_Assignment.var;
2010-02-06, by wenzelm
removed slightly adhoc single-assignment feature, cf. structure Single_Assignment;
2010-02-06, by wenzelm
explicit representation of single-assignment variables;
2010-02-06, by wenzelm
fixed spelling;
2010-02-06, by wenzelm
removed unused "boundary" of Table/Graph.get_first;
2010-02-06, by wenzelm
proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
2010-02-06, by wenzelm
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2010-02-06, by wenzelm
misc tuning;
2010-02-06, by wenzelm
merged
2010-02-06, by haftmann
adjusted to changeset 118b41bba42b5
2010-02-06, by haftmann
tuned font handling;
2010-02-06, by wenzelm
updated versions of requirements;
2010-02-05, by wenzelm
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
2010-02-05, by wenzelm
eliminated self intersection and non-integer coordinates;
2010-02-05, by wenzelm
try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
2010-02-05, by wenzelm
updated generated files;
2010-02-05, by wenzelm
merged
2010-02-05, by wenzelm
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
2010-02-04, by hoelzl
four changes to Nitpick:
2010-02-04, by blanchet
capture error messages (of SMT solvers)
2010-02-02, by boehmes
updated dependencies
2010-02-02, by boehmes
merged
2010-02-02, by boehmes
updated SMT certificates
2010-02-02, by boehmes
updated examples due to changes in the way SMT certificates are stored
2010-02-02, by boehmes
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