Mercurial
Mercurial
>
repos
>
isabelle
/ 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.
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
removed dead code
20100227, by huffman
register match functions from domain_constructors.ML
20100227, by huffman
move definition of match combinators to domain_constructors.ML
20100227, by huffman
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
20100227, by huffman
move definition of discriminators to domain_constructors.ML
20100227, by huffman
move proofs of when_rews intro domain_constructors.ML
20100227, by huffman
moved proofs of dist_les and dist_eqs to domain_constructors.ML
20100227, by huffman
move proofs of casedist into domain_constructors.ML
20100227, by huffman
move proofs of injects and inverts to domain_constructors.ML
20100226, by huffman
reuse vars_of function
20100226, by huffman
remove unnecessary stuff from argument to add_constructors function
20100226, by huffman
reorder sections
20100226, by huffman
move proof of con_rews into domain_constructor.ML
20100226, by huffman
don't bother returning con_defs
20100226, by huffman
move constructorspecific stuff to a separate function
20100226, by huffman
less
more

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