2010-12-02 hoelzl Moved theorems to appropriate place.
2010-12-02 hoelzl Shorter definition for positive_integral.
2010-12-02 hoelzl Move SUP_commute, SUP_less_iff to HOL image;
2010-12-01 hoelzl Generalized simple_functionD and less_SUP_iff.
2010-12-01 hoelzl Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01 hoelzl Replace algebra_eqI by algebra.equality;
2010-12-02 blanchet 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 wenzelm merged
2010-12-02 nipkow coercions
2010-12-01 nipkow merged
2010-12-01 nipkow moved activation of coercion inference into RealDef and declared function real a coercion.
2010-12-01 hoelzl Corrected IsaMakefile
2010-12-01 hoelzl merged
2010-12-01 hoelzl Updated NEWS
2010-12-01 hoelzl More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01 hoelzl Support product spaces on sigma finite measures.
2010-12-01 haftmann merged
2010-12-01 haftmann use type constructor as name for variable
2010-12-01 haftmann optional explicit prefix for type mapper theorems
2010-12-01 haftmann file for package tool type_mapper carries the same name as its Isar command
2010-12-01 huffman merged
2010-12-01 huffman domain package generates non-authentic syntax rules for parsing only
2010-12-02 wenzelm builtin time bounds (again);
2010-12-02 wenzelm tuned;
2010-12-01 wenzelm more abstract handling of Time properties;
2010-12-01 wenzelm store tooltip-dismiss-delay as Double(seconds);
2010-12-01 wenzelm more abstract/uniform handling of time, preferring seconds as Double;
2010-12-01 wenzelm merged
2010-12-01 haftmann NEWS
2010-12-01 wenzelm just one HOLogic.mk_comp;
2010-12-01 wenzelm more direct use of binder_types/body_type;
2010-12-01 wenzelm tuned;
2010-12-01 wenzelm simplified HOL.eq simproc matching;
2010-12-01 wenzelm tuned;
2010-12-01 wenzelm just one Term.dest_funT;
2010-12-01 wenzelm activate subtyping/coercions in theory Complex_Main;
2010-12-01 wenzelm simplified equality on pairs of types;
2010-12-01 wenzelm more precise dependencies;
2010-11-29 traytel two-staged architecture for subtyping;
2010-12-01 huffman merged
2010-11-30 huffman change cpodef-generated cont_Rep rules to cont2cont format
2010-11-30 huffman internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
2010-11-30 huffman remove gratuitous semicolons from ML code
2010-11-30 huffman add continuity lemma for List.map
2010-11-30 huffman simplify predomain instances
2010-11-30 boehmes merged
2010-11-30 boehmes split up Z3 models into constraints on free variables and constant definitions;
2010-11-30 haftmann code preprocessor setup for numerals on word type;
2010-11-30 haftmann merged
2010-11-30 haftmann adaptions to changes in Equiv_Relation.thy
2010-11-30 haftmann adapted fragile proof
2010-11-30 haftmann adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
2010-11-30 haftmann adaptions to changes in Equiv_Relation.thy
2010-11-30 haftmann merged
2010-11-30 haftmann more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-30 haftmann adapted proofs to slightly changed definitions of congruent(2)
2010-11-29 haftmann reorienting iff in Quotient_rel prevents simplifier looping;
2010-11-29 haftmann replaced slightly odd locale congruent2 by plain definition
2010-11-29 haftmann replaced slightly odd locale congruent by plain definition
2010-11-29 haftmann equivI has replaced equiv.intro
2010-11-29 haftmann moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29 haftmann moved generic definitions about relations from Quotient.thy to Predicate;
2010-11-29 haftmann moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-30 huffman simplify proof of LIMSEQ_unique
2010-11-30 huffman use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-11-30 huffman merged
2010-11-29 huffman instance list :: (discrete_cpo) discrete_cpo;
2010-11-29 boehmes merged
2010-11-29 boehmes also support higher-order rules for Z3 proof reconstruction
2010-11-29 wenzelm merged
2010-11-29 haftmann less ghc-specific pragma
2010-11-29 haftmann tuned
2010-11-29 wenzelm updated generated files;
2010-11-29 wenzelm added document antiquotation @{file};
2010-11-28 wenzelm Parse.liberal_name for document antiquotations and attributes;
2010-11-28 wenzelm ML results: enter before printing (cf. Poly/ML SVN 1218);
2010-11-28 wenzelm merged
2010-11-28 huffman merged
2010-11-28 huffman merged
2010-11-28 huffman change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec
2010-11-28 huffman add lemma cont2cont_if_bottom
2010-11-28 wenzelm added Parse.literal_fact with proper inner_syntax markup (source position);
2010-11-28 wenzelm tuned signature;
2010-11-28 wenzelm less frequent sidekick parsing, which is relatively slow;
2010-11-28 wenzelm basic setup for bundled Java runtime;
2010-11-28 wenzelm updated reference platforms;
2010-11-28 wenzelm merged
2010-11-28 nipkow merged
2010-11-28 nipkow gave more standard finite set rules simp and intro attribute
2010-11-28 wenzelm more permissive Isabelle_System.mkdir;
2010-11-28 wenzelm added 'syntax_declaration' command;
2010-11-28 wenzelm more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
2010-11-28 wenzelm superficial tuning;
2010-11-28 wenzelm updated versions;
2010-11-28 wenzelm recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-28 wenzelm follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);
2010-11-28 krauss removed HOLCF for now as explicit component
2010-11-28 huffman fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-28 huffman update web description of HOLCF;
2010-11-28 huffman remove HOLCF from build script, since it no longer works
2010-11-28 huffman moved directory src/HOLCF to src/HOL/HOLCF;
2010-11-27 huffman merged
2010-11-27 huffman rename Pcpodef.thy to Cpodef.thy;
2010-11-27 huffman renamed several HOLCF theorems (listed in NEWS)
2010-11-27 huffman rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
2010-11-27 huffman rename rep_contlub lemmas to rep_lub
2010-11-27 huffman rename function 'match_UU' to 'match_bottom'
2010-11-27 huffman rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27 haftmann merged
2010-11-27 haftmann merged
2010-11-27 haftmann typscheme with signatures is inappropriate when building empty certificate;
2010-11-27 haftmann merged
(0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 +10000 +30000 tip