isabelle: Graph

merged
2010-12-02, by huffman
tuned cpodef code
2010-12-01, by huffman
reformulate lemma preorder.ex_ideal, and use it for typedefs
2010-12-01, by huffman
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
2010-12-02, by hoelzl
merged
2010-12-02, by haftmann
adapted expected value to more idiomatic numeral representation
2010-12-02, by haftmann
corrected representation for code_numeral numerals
2010-12-02, by haftmann
separate term_of function for integers -- more canonical representation of negative integers
2010-12-02, by haftmann
merged
2010-12-02, by hoelzl
Use coercions in Approximation (by Dmitriy Traytel).
2010-12-02, by hoelzl
more antiquotations;
2010-12-02, by wenzelm
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02, by wenzelm
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-12-02, by wenzelm
merged
2010-12-02, by wenzelm
merged
2010-12-02, by hoelzl
generalized simple_functionD
2010-12-02, by hoelzl
Moved theorems to appropriate place.
2010-12-02, by hoelzl
Shorter definition for positive_integral.
2010-12-02, by hoelzl
Move SUP_commute, SUP_less_iff to HOL image;
2010-12-02, by hoelzl
Generalized simple_functionD and less_SUP_iff.
2010-12-01, by hoelzl
Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01, by hoelzl
Replace algebra_eqI by algebra.equality;
2010-12-01, by hoelzl
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
2010-12-02, by blanchet
merged
2010-12-02, by wenzelm
coercions
2010-12-02, by nipkow
merged
2010-12-01, by nipkow
moved activation of coercion inference into RealDef and declared function real a coercion.
2010-12-01, by nipkow
Corrected IsaMakefile
2010-12-01, by hoelzl
merged
2010-12-01, by hoelzl
Updated NEWS
2010-12-01, by hoelzl
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01, by hoelzl
Support product spaces on sigma finite measures.
2010-12-01, by hoelzl
merged
2010-12-01, by haftmann
use type constructor as name for variable
2010-12-01, by haftmann
optional explicit prefix for type mapper theorems
2010-12-01, by haftmann
file for package tool type_mapper carries the same name as its Isar command
2010-12-01, by haftmann
merged
2010-12-01, by huffman
domain package generates non-authentic syntax rules for parsing only
2010-12-01, by huffman
builtin time bounds (again);
2010-12-02, by wenzelm
tuned;
2010-12-02, by wenzelm
more abstract handling of Time properties;
2010-12-01, by wenzelm
store tooltip-dismiss-delay as Double(seconds);
2010-12-01, by wenzelm
more abstract/uniform handling of time, preferring seconds as Double;
2010-12-01, by wenzelm
merged
2010-12-01, by wenzelm
NEWS
2010-12-01, by haftmann
just one HOLogic.mk_comp;
2010-12-01, by wenzelm
more direct use of binder_types/body_type;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
simplified HOL.eq simproc matching;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
just one Term.dest_funT;
2010-12-01, by wenzelm
activate subtyping/coercions in theory Complex_Main;
2010-12-01, by wenzelm
simplified equality on pairs of types;
2010-12-01, by wenzelm
more precise dependencies;
2010-12-01, by wenzelm
two-staged architecture for subtyping;
2010-11-29, by traytel
merged
2010-11-30, by huffman
change cpodef-generated cont_Rep rules to cont2cont format
2010-11-30, by huffman
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
2010-11-30, by huffman
remove gratuitous semicolons from ML code
2010-11-30, by huffman
add continuity lemma for List.map
2010-11-30, by huffman
simplify predomain instances
2010-11-30, by huffman
merged
2010-11-30, by boehmes
split up Z3 models into constraints on free variables and constant definitions;
2010-11-30, by boehmes
code preprocessor setup for numerals on word type;
2010-11-30, by haftmann
merged
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
adapted fragile proof
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
merged
2010-11-30, by haftmann
more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-30, by haftmann
adapted proofs to slightly changed definitions of congruent(2)
2010-11-30, by haftmann
reorienting iff in Quotient_rel prevents simplifier looping;
2010-11-29, by haftmann
replaced slightly odd locale congruent2 by plain definition
2010-11-29, by haftmann
replaced slightly odd locale congruent by plain definition
2010-11-29, by haftmann
equivI has replaced equiv.intro
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
moved generic definitions about relations from Quotient.thy to Predicate;
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
simplify proof of LIMSEQ_unique
2010-11-30, by huffman
use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-11-30, by huffman
merged
2010-11-30, by huffman
instance list :: (discrete_cpo) discrete_cpo;
2010-11-29, by huffman
merged
2010-11-30, by boehmes
also support higher-order rules for Z3 proof reconstruction
2010-11-29, by boehmes
merged
2010-11-29, by wenzelm
less ghc-specific pragma
2010-11-29, by haftmann
tuned
2010-11-29, by haftmann
updated generated files;
2010-11-29, by wenzelm
added document antiquotation @{file};
2010-11-29, by wenzelm
Parse.liberal_name for document antiquotations and attributes;
2010-11-28, by wenzelm
ML results: enter before printing (cf. Poly/ML SVN 1218);
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by huffman
merged
2010-11-28, by huffman
change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec
2010-11-28, by huffman
add lemma cont2cont_if_bottom
2010-11-27, by huffman
added Parse.literal_fact with proper inner_syntax markup (source position);
2010-11-28, by wenzelm
tuned signature;
2010-11-28, by wenzelm
less frequent sidekick parsing, which is relatively slow;
2010-11-28, by wenzelm
basic setup for bundled Java runtime;
2010-11-28, by wenzelm
updated reference platforms;
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by nipkow
gave more standard finite set rules simp and intro attribute
2010-11-28, by nipkow
more permissive Isabelle_System.mkdir;
2010-11-28, by wenzelm
added 'syntax_declaration' command;
2010-11-28, by wenzelm
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
2010-11-28, by wenzelm
superficial tuning;
2010-11-28, by wenzelm
updated versions;
2010-11-28, by wenzelm
recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-28, by wenzelm
follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);
2010-11-28, by wenzelm
removed HOLCF for now as explicit component
2010-11-28, by krauss
fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-27, by huffman
update web description of HOLCF;
2010-11-27, by huffman
remove HOLCF from build script, since it no longer works
2010-11-27, by huffman
moved directory src/HOLCF to src/HOL/HOLCF;
2010-11-27, by huffman
merged
2010-11-27, by huffman
rename Pcpodef.thy to Cpodef.thy;
2010-11-27, by huffman
renamed several HOLCF theorems (listed in NEWS)
2010-11-27, by huffman
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
2010-11-27, by huffman
rename rep_contlub lemmas to rep_lub
2010-11-27, by huffman
rename function 'match_UU' to 'match_bottom'
2010-11-27, by huffman
rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27, by huffman
merged
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
typscheme with signatures is inappropriate when building empty certificate;
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
corrected: use canonical variables of type scheme uniformly
2010-11-27, by haftmann
tuned
2010-11-27, by haftmann
merged
2010-11-26, by haftmann
consider sort constraints for datatype constructors when constructing the empty equation certificate;
2010-11-26, by haftmann
tuned example
2010-11-26, by haftmann
merged
2010-11-27, by wenzelm
updated generated documents
2010-11-27, by haftmann
added equation for Queue;
2010-11-27, by haftmann
added evaluation section
2010-11-27, by haftmann
tuned formatting;
2010-11-27, by haftmann
added label
2010-11-27, by haftmann
more thorough process termination (cf. Scala version);
2010-11-27, by wenzelm
prefer Isabelle/ML concurrency elements;
2010-11-27, by wenzelm
removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-27, by wenzelm
more proper int wrappers;
2010-11-27, by wenzelm
explicit check for requirement;
2010-11-27, by wenzelm
more basic Isabelle_System.mkdir;
2010-11-27, by wenzelm
tuned;
2010-11-27, by wenzelm
more explicit Isabelle_System operations;
2010-11-27, by wenzelm
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
2010-11-27, by wenzelm
moved file identification to thy_load.ML (where it is actually used);
2010-11-27, by wenzelm
removed some old settings;
2010-11-27, by wenzelm
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
2010-11-27, by wenzelm
merged
2010-11-26, by huffman
remove map function names from domain package theory data
2010-11-26, by huffman
isar-style proof for lemma contI2
2010-11-26, by huffman
remove case combinator for fixrec match type
2010-11-26, by huffman
declare more simp rules for powerdomains
2010-11-26, by huffman
merged;
2010-11-27, by wenzelm
merged
2010-11-26, by haftmann
strict forall2
2010-11-26, by haftmann
nbe decides equality of abstractions by extensionality
2010-11-26, by haftmann
eliminated some generated comments;
2010-11-26, by wenzelm
merged
2010-11-26, by wenzelm
merged
2010-11-26, by haftmann
keep type variable arguments of datatype constructors in bookkeeping
2010-11-26, by haftmann
document changes in Nitpick and MESON/Metis
2010-11-26, by blanchet
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
2010-11-26, by blanchet
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-26, by blanchet
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26, by wenzelm
just one version of fold_rev2;
2010-11-26, by wenzelm
explicit use of unprefix;
2010-11-26, by wenzelm
keep private things private, without comments;
2010-11-26, by wenzelm
eliminated some clones of eq_list;
2010-11-26, by wenzelm
merged
2010-11-26, by nipkow
new lemma
2010-11-26, by nipkow
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-26, by wenzelm
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-11-26, by wenzelm
discontinued global "Isabelle" symlink, to make each distribution even more self-contained;
2010-11-26, by wenzelm
more correct spelling;
2010-11-26, by wenzelm
globbing constant expressions use more idiomatic underscore rather than star
2010-11-26, by haftmann
globbing constant expressions use more idiomatic underscore rather than star;
2010-11-26, by haftmann
datatype constructor glob for code_reflect
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-25, by haftmann
toplevel deresolving for flat module name space
2010-11-25, by haftmann
merged
2010-11-26, by hoelzl
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-23, by hoelzl
Replace surj by abbreviation; remove surj_on.
2010-11-22, by hoelzl
adjust Sledgehammer/SMT fudge factor
2010-11-26, by blanchet
clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);
2010-11-25, by wenzelm
merge
2010-11-25, by blanchet
cosmetics
2010-11-25, by blanchet
eta-reduce on the fly to prevent an exception
2010-11-25, by blanchet
merged
2010-11-25, by nipkow
Added the simplest finite Ramsey theorem
2010-11-25, by nipkow
reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions
2010-11-25, by blanchet
set Metis option on correct context, lest it be ignored
2010-11-25, by blanchet
make "debug" mode of Sledgehammer/SMT more liberal
2010-11-25, by blanchet
fix check for builtinness of 0 and 1 -- these aren't functions
2010-11-25, by blanchet
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
2010-11-25, by blanchet
document requirement on theory import
2010-11-24, by blanchet
corrected abd4e7358847 where SOMEthing went utterly wrong
2010-11-24, by haftmann
merged
2010-11-24, by boehmes
swap names for built-in tester functions (to better reflect the intuition of what they do);
2010-11-24, by boehmes
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
2010-11-24, by boehmes
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-24, by blanchet
removing Enum.in_enum from the claset
2010-11-24, by bulwahn
merged
2010-11-24, by boehmes
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-24, by boehmes
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
2010-11-24, by boehmes
announcing some latest change (d40b347d5b0b)
2010-11-24, by bulwahn
merged
2010-11-23, by blanchet
more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-23, by blanchet
merged
2010-11-23, by haftmann
merged
2010-11-22, by haftmann
adhere established Collect/mem convention more closely
2010-11-22, by haftmann
merged
2010-11-22, by haftmann
replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22, by haftmann
renamed slightly ambivalent crel to effect
2010-11-22, by haftmann
disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day
2010-11-23, by blanchet
more precise error handling for Z3;
2010-11-23, by blanchet
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
2010-11-23, by blanchet
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
2010-11-23, by blanchet