Mercurial
Mercurial
>
repos
>
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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
removed interrupt handling that violates Isabelle/ML exception model
20101203, by bulwahn
corrected indentation
20101203, by bulwahn
tuned
20101203, by bulwahn
smallvalue_generator are defined quick via oracle or sound via function package
20101203, by bulwahn
adding shorter output syntax for the finite types of quickcheck
20101203, by bulwahn
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
20101203, by bulwahn
changed order of lemmas to overwrite the general code equation with the nbespecific one
20101203, by bulwahn
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
20101203, by hoelzl
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
20101203, by wenzelm
updated latex dependencies (cf. 7d88ebdce380);
20101203, by wenzelm
tuned README;
20101203, by wenzelm
isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;
20101202, by wenzelm
proper theory name (cf. e84f82418e09);
20101202, by wenzelm
merged;
20101202, by wenzelm
merged
20101202, by huffman
tuned cpodef code
20101201, by huffman
reformulate lemma preorder.ex_ideal, and use it for typedefs
20101201, by huffman
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
20101202, by hoelzl
merged
20101202, by haftmann
adapted expected value to more idiomatic numeral representation
20101202, by haftmann
corrected representation for code_numeral numerals
20101202, by haftmann
separate term_of function for integers  more canonical representation of negative integers
20101202, by haftmann
merged
20101202, by hoelzl
Use coercions in Approximation (by Dmitriy Traytel).
20101202, by hoelzl
more antiquotations;
20101202, by wenzelm
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
20101202, by wenzelm
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
20101202, by wenzelm
merged
20101202, by wenzelm
merged
20101202, by hoelzl
generalized simple_functionD
20101202, by hoelzl
Moved theorems to appropriate place.
20101202, by hoelzl
Shorter definition for positive_integral.
20101202, by hoelzl
Move SUP_commute, SUP_less_iff to HOL image;
20101202, by hoelzl
Generalized simple_functionD and less_SUP_iff.
20101201, by hoelzl
Tuned setup for borel_measurable with min, max and psuminf.
20101201, by hoelzl
Replace algebra_eqI by algebra.equality;
20101201, 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)
20101202, by blanchet
merged
20101202, by wenzelm
coercions
20101202, by nipkow
merged
20101201, by nipkow
moved activation of coercion inference into RealDef and declared function real a coercion.
20101201, by nipkow
Corrected IsaMakefile
20101201, by hoelzl
merged
20101201, by hoelzl
Updated NEWS
20101201, by hoelzl
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
20101201, by hoelzl
Support product spaces on sigma finite measures.
20101201, by hoelzl
merged
20101201, by haftmann
use type constructor as name for variable
20101201, by haftmann
optional explicit prefix for type mapper theorems
20101201, by haftmann
file for package tool type_mapper carries the same name as its Isar command
20101201, by haftmann
merged
20101201, by huffman
domain package generates nonauthentic syntax rules for parsing only
20101201, by huffman
builtin time bounds (again);
20101202, by wenzelm
tuned;
20101202, by wenzelm
more abstract handling of Time properties;
20101201, by wenzelm
store tooltipdismissdelay as Double(seconds);
20101201, by wenzelm
more abstract/uniform handling of time, preferring seconds as Double;
20101201, by wenzelm
merged
20101201, by wenzelm
NEWS
20101201, by haftmann
just one HOLogic.mk_comp;
20101201, by wenzelm
more direct use of binder_types/body_type;
20101201, by wenzelm
tuned;
20101201, by wenzelm
simplified HOL.eq simproc matching;
20101201, by wenzelm
tuned;
20101201, by wenzelm
just one Term.dest_funT;
20101201, by wenzelm
activate subtyping/coercions in theory Complex_Main;
20101201, by wenzelm
simplified equality on pairs of types;
20101201, by wenzelm
more precise dependencies;
20101201, by wenzelm
twostaged architecture for subtyping;
20101129, by traytel
merged
20101130, by huffman
change cpodefgenerated cont_Rep rules to cont2cont format
20101130, by huffman
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
20101130, by huffman
remove gratuitous semicolons from ML code
20101130, by huffman
add continuity lemma for List.map
20101130, by huffman
simplify predomain instances
20101130, by huffman
merged
20101130, by boehmes
split up Z3 models into constraints on free variables and constant definitions;
20101130, by boehmes
code preprocessor setup for numerals on word type;
20101130, by haftmann
merged
20101130, by haftmann
adaptions to changes in Equiv_Relation.thy
20101130, by haftmann
adapted fragile proof
20101130, by haftmann
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
20101130, by haftmann
adaptions to changes in Equiv_Relation.thy
20101130, by haftmann
merged
20101130, by haftmann
more systematic and compact proofs on type relation operators using natural deduction rules
20101130, by haftmann
adapted proofs to slightly changed definitions of congruent(2)
20101130, by haftmann
reorienting iff in Quotient_rel prevents simplifier looping;
20101129, by haftmann
replaced slightly odd locale congruent2 by plain definition
20101129, by haftmann
replaced slightly odd locale congruent by plain definition
20101129, by haftmann
equivI has replaced equiv.intro
20101129, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
20101129, by haftmann
moved generic definitions about relations from Quotient.thy to Predicate;
20101129, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
20101129, by haftmann
simplify proof of LIMSEQ_unique
20101130, by huffman
use new 'file' antiquotation for reference to Dedekind_Real.thy
20101130, by huffman
merged
20101130, by huffman
instance list :: (discrete_cpo) discrete_cpo;
20101129, by huffman
merged
20101130, by boehmes
also support higherorder rules for Z3 proof reconstruction
20101129, by boehmes
merged
20101129, by wenzelm
less ghcspecific pragma
20101129, by haftmann
tuned
20101129, by haftmann
updated generated files;
20101129, by wenzelm
added document antiquotation @{file};
20101129, by wenzelm
Parse.liberal_name for document antiquotations and attributes;
20101128, by wenzelm
ML results: enter before printing (cf. Poly/ML SVN 1218);
20101128, by wenzelm
merged
20101128, by wenzelm
merged
20101128, by huffman
merged
20101128, by huffman
change match_bottom_simps to produce ifthenelse, making more uses of bottompatterns work with fixrec
20101128, by huffman
add lemma cont2cont_if_bottom
20101127, by huffman
added Parse.literal_fact with proper inner_syntax markup (source position);
20101128, by wenzelm
tuned signature;
20101128, by wenzelm
less frequent sidekick parsing, which is relatively slow;
20101128, by wenzelm
basic setup for bundled Java runtime;
20101128, by wenzelm
updated reference platforms;
20101128, by wenzelm
merged
20101128, by wenzelm
merged
20101128, by nipkow
gave more standard finite set rules simp and intro attribute
20101128, by nipkow
more permissive Isabelle_System.mkdir;
20101128, by wenzelm
less
more

(0)
30000
10000
3000
1000
120
+120
+1000
+3000
+10000
+30000
tip