isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

rename type 'a net to 'a filter, following standard mathematical terminology
2011-08-08, by huffman
HOLCF: fix warnings about unreferenced identifiers
2011-08-08, by huffman
remove duplicate lemmas
2011-08-08, by huffman
merged
2011-08-08, by huffman
fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)
2011-08-08, by huffman
generalize sequence lemmas
2011-08-08, by huffman
generalize more lemmas about compactness
2011-08-08, by huffman
generalize compactness equivalence lemmas
2011-08-08, by huffman
lemma bolzano_weierstrass_imp_compact
2011-08-08, by huffman
class perfect_space inherits from topological_space;
2011-08-08, by huffman
merged
2011-08-08, by wenzelm
import constant folding theory into IMP
2011-08-08, by kleing
make syntax ambiguity warnings a config option
2011-08-06, by kleing
add lemmas INF_image, SUP_image
2011-08-08, by huffman
declare {INF,SUP}_empty [simp]
2011-08-08, by huffman
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
2011-08-08, by huffman
standard theorem naming scheme: complex_eqI, complex_eq_iff
2011-08-08, by huffman
moved division ring stuff from Rings.thy to Fields.thy
2011-08-08, by huffman
Library/Product_ord: wellorder instance for products
2011-08-08, by huffman
modernized file proof_checker.ML;
2011-08-08, by wenzelm
tuned thm_of_proof: build lookup table within closure;
2011-08-08, by wenzelm
added Reconstruct.proof_of convenience;
2011-08-08, by wenzelm
ship message in one piece;
2011-08-08, by wenzelm
misc tuning -- eliminated old-fashioned rep_thm;
2011-08-08, by wenzelm
modernized strcture Proof_Checker;
2011-08-08, by wenzelm
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
2011-08-08, by wenzelm
updated imports;
2011-08-08, by wenzelm
proper signature;
2011-08-08, by wenzelm
made SML/NJ happy;
2011-08-08, by wenzelm
slightly more uniform messages;
2011-08-08, by wenzelm
avoid pointless completion of illegal control commands;
2011-08-08, by wenzelm
removed old expand_fun_eq
2011-08-08, by nipkow
fixed index entry
2011-08-08, by nipkow
removed old recdef and types usage
2011-08-08, by nipkow
merged
2011-08-08, by nipkow
extended user-level attribute case_names with names for case hypotheses
2011-08-06, by nipkow
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-08-01, by nipkow
workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;
2011-08-07, by wenzelm
updated version information;
2011-08-07, by wenzelm
fixed document;
2011-08-07, by wenzelm
tuned order: pushing INF and SUP to Inf and Sup
2011-08-05, by haftmann
tuned order: pushing INF and SUP to Inf and Sup
2011-08-05, by haftmann
generalized lemmas to complete lattices
2011-08-05, by haftmann
merged
2011-08-05, by Andreas Lochbihler
replace old SML code generator by new code generator in MicroJava/J
2011-08-05, by Andreas Lochbihler
new state syntax with less conflicts
2011-08-04, by kleing
replace old SML code generator by new code generator in MicroJava/JVM and /BV
2011-08-05, by Andreas Lochbihler
merged
2011-08-05, by haftmann
more fine-granular instantiation
2011-08-04, by haftmann
solving duality problem for complete_distrib_lattice; tuned
2011-08-04, by haftmann
merged
2011-08-04, by berghofe
Pending FDL types may now be associated with Isabelle types as well.
2011-08-04, by berghofe
tuned orthography
2011-08-04, by haftmann
avoid yet unknown fact antiquotation
2011-08-04, by haftmann
NEWS
2011-08-04, by haftmann
more specific instantiation
2011-08-03, by haftmann
tuned
2011-08-03, by haftmann
class complete_distrib_lattice
2011-08-03, by haftmann
NEWS
2011-08-03, by bulwahn
removing value invocations with the SML code generator
2011-08-03, by bulwahn
removing the SML evaluator
2011-08-03, by bulwahn
fixed wrong isubs in IMP/Types
2011-08-03, by kleing
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
2011-08-02, by huffman
NEWS: fix typo
2011-08-02, by huffman
updated unchecked forward reference
2011-08-02, by krauss
replaced Nitpick's hardwired basic_ersatz_table by context data
2011-08-02, by krauss
NEWS
2011-08-02, by krauss
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02, by krauss
moved recdef package to HOL/Library/Old_Recdef.thy
2011-08-02, by krauss
added dynamic ersatz_table to Nitpick's data slot
2011-08-02, by krauss
eliminated obsolete recdef/wfrec related declarations
2011-08-02, by krauss
more consistent naming in IMP/Comp_Rev
2011-08-01, by kleing
merged
2011-08-01, by haftmann
tuned proofs
2011-07-30, by haftmann
tuned proofs
2011-07-29, by haftmann
new theory HOL/Library/Product_Lattice.thy
2011-08-01, by huffman
domain package: more informative error message for illegal indirect recursion
2011-07-31, by huffman
compiler proof cleanup
2011-07-28, by kleing
added helpers for "All" and "Ex"
2011-07-28, by blanchet
put parentheses around non-trivial metis call
2011-07-28, by blanchet
no needless mangling
2011-07-28, by blanchet
resolved code_pred FIXME in IMP; clearer notation for exec_n
2011-07-28, by kleing
clean up temporary directory hack
2011-07-28, by blanchet
tuning
2011-07-28, by blanchet
fixed lambda concealing
2011-07-28, by blanchet
make SML/NJ happy
2011-07-28, by blanchet
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
2011-07-28, by hoelzl
document coercions
2011-07-28, by noschinl
rudimentary documentation of the quotient package in the isar reference manual
2011-07-27, by bulwahn
to_nat is injective on arbitrary domains
2011-07-27, by hoelzl
finite vimage on arbitrary domains
2011-07-27, by hoelzl
updated Sledgehammer documentation
2011-07-26, by blanchet
renamed "preds" encodings to "guards"
2011-07-26, by blanchet
more precise dependencies
2011-07-26, by bulwahn
further worked around LEO-II parser limitation, with eta-expansion
2011-07-26, by blanchet
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
2011-07-26, by blanchet
no need for existential witnesses for sorts in TFF and THF formats
2011-07-26, by blanchet
mangle "undefined"
2011-07-26, by blanchet
tuning -- remove useless function (at this point combinators are already in)
2011-07-26, by blanchet
remove spurious message
2011-07-26, by blanchet
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
2011-07-26, by blanchet
merged
2011-07-26, by Andreas Lochbihler
fixed code generator setup in List_Cset
2011-07-26, by Andreas Lochbihler
enat is a complete_linorder instance
2011-07-26, by hoelzl
merged
2011-07-26, by Andreas Lochbihler
Add theory for setting up monad syntax for Cset
2011-07-26, by Andreas Lochbihler
merged
2011-07-26, by bulwahn
removing expectations from quickcheck example
2011-07-26, by bulwahn
adding remarks after static inspection of the invocation of the SML code generator
2011-07-26, by bulwahn
merged
2011-07-26, by Andreas Lochbihler
added operations to Cset with code equations in backing implementations
2011-07-25, by Andreas Lochbihler
merged
2011-07-25, by haftmann
adjusted to tailored version of ball_simps
2011-07-25, by haftmann
adjusted to tailored version of bex_simps
2011-07-24, by haftmann
more coherent structure in and across theories
2011-07-24, by haftmann
declare "undefined" constant
2011-07-25, by blanchet
make compile
2011-07-25, by blanchet
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
2011-07-25, by blanchet
tuning
2011-07-25, by blanchet
introduced hybrid lambda translation
2011-07-25, by blanchet