Mercurial
Mercurial
>
repos
>
testboard
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+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.
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
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip