2009-11-21 ballarin Publication details and minor correction of the text.
2009-11-21 ballarin Removed obsolete comment.
2009-11-21 ballarin Merged.
2009-11-21 ballarin More tests for locale interpretation.
2009-11-21 wenzelm adapted local theory operations -- eliminated odd kind;
2009-11-21 wenzelm minimal Poly/ML startup script;
2009-11-21 wenzelm explicitly mark some legacy freeze operations;
2009-11-21 wenzelm minimal test of current repository version;
2009-11-21 wenzelm slightly longer log tail;
2009-11-21 kleing add explicit platform check to wwwfind tool
2009-11-21 kleing adjusted help text
2009-11-21 kleing wwwfind support currently for Linux only
2009-11-20 huffman make repdef work without (open) option
2009-11-20 huffman NEWS: HOLCF changes since the last release
2009-11-20 wenzelm removed hard tabs from text (not pattern);
2009-11-20 wenzelm standardized headers;
2009-11-20 wenzelm provide standard isabelle make targets;
2009-11-20 wenzelm merged
2009-11-20 wenzelm load ML directly into theory Code_Generator (quickcheck also requires this);
2009-11-20 kleing made script executable
2009-11-20 kleing added NEWS item for wwwfind
2009-11-20 kleing WWW_Find component: find_theorems via web browser
2009-11-20 wenzelm merged
2009-11-20 nipkow merged
2009-11-20 nipkow Rene tuned proof
2009-11-20 huffman example theory for new domain package
2009-11-20 huffman thy_decl outer syntax for repdef
2009-11-20 huffman merged
2009-11-20 huffman nicer warning message for indirect-recursive domain definitions
2009-11-20 huffman store map_ID thms in theory data; automate proofs of reach lemmas
2009-11-20 huffman add map_ID lemmas
2009-11-20 huffman domain_isomorphism package defines combined copy function
2009-11-20 nipkow merged
2009-11-20 nipkow added Rene Thiemann's normalize function
2009-11-20 nipkow added lemma
2009-11-20 huffman merged
2009-11-20 huffman domain_isomorphism package defines copy functions
2009-11-20 huffman copy_of_dtyp uses map table from theory data
2009-11-20 huffman Domain.thy imports Representable.thy
2009-11-20 huffman fix definitions of copy combinators
2009-11-19 huffman clean up indentation; add 'definitional' option flag
2009-11-19 huffman rename generated abs_iso, rep_iso lemmas
2009-11-19 huffman clean up indentation
2009-11-19 huffman add dependency on domain_isomorphism.ML
2009-11-19 huffman set up domain_isomorphism package in Representable.thy
2009-11-19 huffman automate proofs of map_ID theorems
2009-11-19 huffman change Theory.requires
2009-11-19 huffman use theory data for REP_simps and isodefl_rules
2009-11-19 huffman replace defl_tab and map_tab with theory data
2009-11-19 huffman separate conjuncts of isodefl theorem
2009-11-19 huffman automate isodefl proof
2009-11-19 huffman change example to use recursion with continuous function space
2009-11-19 huffman add lemma isodefl_cprod
2009-11-19 huffman automate definition of map functions; remove unused code
2009-11-19 huffman change naming convention for deflation combinators
2009-11-19 huffman add new makefile dependencies
2009-11-19 huffman prove isomorphism and isodefl rules
2009-11-19 huffman avoid using csplit; define copy functions exactly like the current domain package
2009-11-19 huffman merged
2009-11-19 huffman remove one_typ and tr_typ; add abs/rep lemmas
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip