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 JavaScript-enabled browsers.
merged
2010-03-02, by huffman
re-enable bisim code, now in domain_theorems.ML
2010-03-02, by huffman
add missing rule to case_strict proof script
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
domain package no longer generates copy functions; all proofs use take functions instead
2010-03-02, by huffman
need to explicitly include REP_convex
2010-03-01, by huffman
add lemma lub_eq
2010-03-01, by huffman
add lemmas about ssum_map and sprod_map
2010-03-01, by huffman
generate take_take rules
2010-03-01, by huffman
add function define_take_functions
2010-03-01, by huffman
add missing strictify rule to proof script
2010-03-01, by huffman
qualify constructor names with type name
2010-03-01, by huffman
move definition of case combinator to domain_constructors.ML
2010-03-01, by huffman
remove dependence on Domain_Library
2010-03-01, by huffman
more uses of function get_vars
2010-03-01, by huffman
add functions get_vars, get_vars_avoiding
2010-03-01, by huffman
move proofs of pat_rews to domain_constructors.ML
2010-03-01, by huffman
add_domain_constructors takes iso_info record as argument
2010-02-28, by huffman
domain_isomorphism package proves deflation rules for map functions
2010-02-28, by huffman
store deflation thms for map functions in theory data
2010-02-28, by huffman
use function list_ccomb
2010-02-28, by huffman
add function define_const
2010-02-28, by huffman
fix infix declarations
2010-02-28, by huffman
move common functions into new file holcf_library.ML
2010-02-28, by huffman
get rid of incomplete pattern match warnings
2010-02-28, by huffman
move some powerdomain stuff into a new file
2010-02-28, by huffman
move case combinator syntax to domain_constructors.ML
2010-02-28, by huffman
remove redundant code
2010-02-28, by huffman
use correct syntax name for pattern combinator
2010-02-28, by huffman
fix output translation for Case syntax
2010-02-28, by huffman
move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-28, by huffman
domain_isomorphism function returns iso_info record
2010-02-27, by huffman
move proofs of match_rews to domain_constructors.ML
2010-02-27, by huffman
remove dead code
2010-02-27, by huffman
removed dead code
2010-02-27, by huffman
register match functions from domain_constructors.ML
2010-02-27, by huffman
move definition of match combinators to domain_constructors.ML
2010-02-27, by huffman
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
2010-02-27, by huffman
move definition of discriminators to domain_constructors.ML
2010-02-27, by huffman
move proofs of when_rews intro domain_constructors.ML
2010-02-27, by huffman
moved proofs of dist_les and dist_eqs to domain_constructors.ML
2010-02-27, by huffman
move proofs of casedist into domain_constructors.ML
2010-02-27, by huffman
move proofs of injects and inverts to domain_constructors.ML
2010-02-26, by huffman
reuse vars_of function
2010-02-26, by huffman
remove unnecessary stuff from argument to add_constructors function
2010-02-26, by huffman
reorder sections
2010-02-26, by huffman
move proof of con_rews into domain_constructor.ML
2010-02-26, by huffman
don't bother returning con_defs
2010-02-26, by huffman
move constructor-specific stuff to a separate function
2010-02-26, by huffman
replace prove_thm function
2010-02-26, by huffman
move proof of compactness rules into domain_constructors.ML
2010-02-26, by huffman
add some convenience functions
2010-02-26, by huffman
rewrite domain package code for selector functions
2010-02-25, by huffman
add function beta_of_def
2010-02-24, by huffman
reorganizing domain package code (in progress)
2010-02-24, by huffman
change domain package's treatment of variable names in theorems to be like datatype package
2010-02-24, by huffman
remove redundant lemma real_minus_half_eq
2010-02-24, by huffman
polished and converted some proofs to Isar style
2010-02-24, by huffman
killed more recdefs
2010-03-02, by krauss
tuned comment
2010-03-01, by krauss
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip