isabelle: Graph

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

made smlnj happy
2010-03-02, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-03-02, by bulwahn
adding HOL-Mutabelle to tests
2010-03-02, by bulwahn
merged
2010-03-03, by haftmann
more explicit naming scheme
2010-03-03, by haftmann
merged
2010-03-02, by huffman
adapt to changed variable name in casedist theorem
2010-03-02, by huffman
remove dependency on domain_syntax.ML
2010-03-02, by huffman
update HOLCF makefile
2010-03-02, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02, by huffman
proof scripts use variable name y for casedist
2010-03-02, by huffman
fixrec and repdef modules import holcf_library
2010-03-02, by huffman
use y as variable name in casedist, like datatype package
2010-03-02, by huffman
proper names for types cfun, sprod, ssum
2010-03-02, by huffman
variable name changed
2010-03-02, by huffman
fix proof script for take_apps so it works with indirect recursion
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
remove unused mixfix component from type cons
2010-03-02, by huffman
cleaned up, added type annotations
2010-03-02, by huffman
remove unused selector field from type arg
2010-03-02, by huffman
add_syntax no longer needs a definitional mode
2010-03-02, by huffman
add_axioms no longer needs a definitional mode
2010-03-02, by huffman
get rid of primes on thy variables
2010-03-02, by huffman
move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02, by huffman
move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02, by huffman
remove map_tab argument to calc_axioms
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
merged
2010-03-02, by paulson
Slightly generalised a theorem
2010-03-02, by paulson
merged
2010-03-02, by paulson
merged
2010-02-19, by paulson
merged
2010-02-19, by paulson
merged
2010-02-05, by paulson
merged
2010-02-04, by paulson
merged
2010-02-02, by paulson
Correction of a tiny error
2010-02-02, by paulson
removed obsolete helper theory
2010-03-02, by krauss
merged
2010-03-02, by haftmann
dropped superfluous naming
2010-03-02, by haftmann
UNIV is not a logical constant
2010-03-02, by huffman
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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle