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.
generalized inj_uminus; added strict_mono_imp_inj_on
20100305, by hoelzl
merged
20100305, by hoelzl
Add Lebesgue integral and probability space.
20100304, by hoelzl
Supremum and Infimum on real intervals
20100304, by hoelzl
Rewrite rules for images of minus of intervals
20100304, by hoelzl
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
20100304, by hoelzl
Added natfloor and floor rules for multiplication and power.
20100304, by hoelzl
Generalized setsum_cases
20100304, by hoelzl
Added vimage_inter_cong
20100304, by hoelzl
merged
20100304, by huffman
move coinductionrelated stuff into function prove_coindunction
20100304, by huffman
add function add_qualified_simp_thm
20100304, by huffman
generate lemma take_below, declare chain_take [simp]
20100303, by huffman
switch to polymlsvn;
20100304, by wenzelm
basic simplification of external_prover signature;
20100304, by wenzelm
tuned;
20100304, by wenzelm
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
20100304, by wenzelm
point to http://hginit.com/
20100304, by wenzelm
Simplified a couple of proofs and corrected a comment
20100304, by paulson
lemmas set_map_of_compr, map_of_inject_set
20100304, by haftmann
merged
20100303, by huffman
merged
20100303, by huffman
remove dead code
20100303, by huffman
add infix declarations
20100303, by huffman
remove unnecessary theorem references
20100303, by huffman
remove copy_of_dtyp from domain_axioms.ML
20100303, by huffman
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
20100303, by huffman
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
20100303, by huffman
add function axiomatize_lub_take
20100303, by huffman
move function mk_lub into holcf_library.ML
20100303, by huffman
added extern_syntax;
20100303, by wenzelm
merged
20100303, by haftmann
more uniform naming conventions
20100303, by haftmann
tuned whitespace
20100303, by haftmann
restructured RBT theory
20100303, by haftmann
stats for atpolytest;
20100303, by wenzelm
proper names for types cfun, sprod, ssum (cf. fa231b86cb1e);
20100303, by wenzelm
merged, resolving some basic conflicts;
20100303, by wenzelm
merged
20100303, by krauss
updated patch for hgweb style: now applies to Mercurial 1.4.3 templates
20100303, by krauss
fix fragile proof using old induction rule (cf. bdf8ad377877)
20100303, by krauss
merged
20100303, by hoelzl
replaced \<bullet> with inner
20100302, by himmelma
tuned
20100302, by himmelma
the ordering on real^1 is linear
20100302, by himmelma
merged
20100303, by bulwahn
made smlnj happy
20100302, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
20100302, by bulwahn
adding HOLMutabelle to tests
20100302, by bulwahn
merged
20100303, by haftmann
more explicit naming scheme
20100303, by haftmann
merged
20100302, by huffman
adapt to changed variable name in casedist theorem
20100302, by huffman
remove dependency on domain_syntax.ML
20100302, by huffman
update HOLCF makefile
20100302, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
20100302, by huffman
proof scripts use variable name y for casedist
20100302, by huffman
fixrec and repdef modules import holcf_library
20100302, by huffman
use y as variable name in casedist, like datatype package
20100302, by huffman
proper names for types cfun, sprod, ssum
20100302, by huffman
variable name changed
20100302, by huffman
fix proof script for take_apps so it works with indirect recursion
20100302, by huffman
remove dead code
20100302, by huffman
remove unused mixfix component from type cons
20100302, by huffman
cleaned up, added type annotations
20100302, by huffman
remove unused selector field from type arg
20100302, by huffman
add_syntax no longer needs a definitional mode
20100302, by huffman
add_axioms no longer needs a definitional mode
20100302, by huffman
get rid of primes on thy variables
20100302, by huffman
move definition of finiteness predicate into domain_take_proofs.ML
20100302, by huffman
move takerelated definitions and proofs to new module; simplify map_of_typ functions
20100302, by huffman
remove map_tab argument to calc_axioms
20100302, by huffman
remove dead code
20100302, by huffman
merged
20100302, by paulson
Slightly generalised a theorem
20100302, by paulson
merged
20100302, by paulson
merged
20100219, by paulson
merged
20100219, by paulson
merged
20100205, by paulson
merged
20100204, by paulson
merged
20100202, by paulson
Correction of a tiny error
20100202, by paulson
removed obsolete helper theory
20100302, by krauss
merged
20100302, by haftmann
dropped superfluous naming
20100302, by haftmann
UNIV is not a logical constant
20100302, by huffman
merged
20100302, by huffman
reenable bisim code, now in domain_theorems.ML
20100302, by huffman
add missing rule to case_strict proof script
20100302, by huffman
remove dead code
20100302, by huffman
domain package no longer generates copy functions; all proofs use take functions instead
20100302, by huffman
need to explicitly include REP_convex
20100301, by huffman
add lemma lub_eq
20100301, by huffman
add lemmas about ssum_map and sprod_map
20100301, by huffman
generate take_take rules
20100301, by huffman
add function define_take_functions
20100301, by huffman
add missing strictify rule to proof script
20100301, by huffman
qualify constructor names with type name
20100301, by huffman
move definition of case combinator to domain_constructors.ML
20100301, by huffman
remove dependence on Domain_Library
20100301, by huffman
more uses of function get_vars
20100301, by huffman
add functions get_vars, get_vars_avoiding
20100301, by huffman
move proofs of pat_rews to domain_constructors.ML
20100301, by huffman
add_domain_constructors takes iso_info record as argument
20100228, by huffman
domain_isomorphism package proves deflation rules for map functions
20100228, by huffman
store deflation thms for map functions in theory data
20100228, by huffman
use function list_ccomb
20100228, by huffman
add function define_const
20100228, by huffman
fix infix declarations
20100228, by huffman
move common functions into new file holcf_library.ML
20100228, by huffman
get rid of incomplete pattern match warnings
20100228, by huffman
move some powerdomain stuff into a new file
20100228, by huffman
move case combinator syntax to domain_constructors.ML
20100228, by huffman
remove redundant code
20100228, by huffman
use correct syntax name for pattern combinator
20100228, by huffman
fix output translation for Case syntax
20100228, by huffman
move definition and syntax of pattern combinators into domain_constructors.ML
20100228, by huffman
domain_isomorphism function returns iso_info record
20100227, by huffman
move proofs of match_rews to domain_constructors.ML
20100227, by huffman
remove dead code
20100227, by huffman
less
more

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