2010-11-19 wenzelm 2010-11-19 total Symbol.explode (cf. 1050315f6ee2);
2010-11-19 wenzelm 2010-11-19 do not export Thy_Load.required, to avoid confusion about the interface;
2010-11-19 huffman 2010-11-19 merged
2010-11-17 huffman 2010-11-17 declare adm_chfin [simp]
2010-11-17 huffman 2010-11-17 add lemma cont_fun; remove unused lemma monofun_app
2010-11-17 huffman 2010-11-17 accumulated NEWS updates for HOLCF
2010-11-17 huffman 2010-11-17 section -> subsection
2010-11-17 huffman 2010-11-17 add lemma adm_prod_case
2010-11-19 paulson 2010-11-19 merged
2010-11-19 paulson 2010-11-19 First-order pattern matching: catch a rogue exception (differing numbers of arguments)
2010-11-19 haftmann 2010-11-19 eval simp rules for predicate type, simplify primitive proofs
2010-11-19 haftmann 2010-11-19 generalized type
2010-11-19 haftmann 2010-11-19 made smlnj happy
2010-11-19 haftmann 2010-11-19 merged
2010-11-18 haftmann 2010-11-18 proper qualification needed due to shadowing on theory merge
2010-11-18 haftmann 2010-11-18 more appropriate name for property
2010-11-18 haftmann 2010-11-18 mapper for sum type
2010-11-18 haftmann 2010-11-18 mapper for option type
2010-11-18 haftmann 2010-11-18 mapper for list type; map_pair replaces prod_fun
2010-11-18 haftmann 2010-11-18 map_pair replaces prod_fun
2010-11-18 haftmann 2010-11-18 mapper for mulitset type
2010-11-18 haftmann 2010-11-18 mapper for mapping type
2010-11-18 haftmann 2010-11-18 mapper for fset type
2010-11-18 haftmann 2010-11-18 mapper for dlist type
2010-11-18 haftmann 2010-11-18 map_fun combinator in theory Fun
2010-11-18 wenzelm 2010-11-18 some updates after 2 years of Mercurial usage;
2010-11-18 blanchet 2010-11-18 mention Sledgehammer with SMT
2010-11-18 blanchet 2010-11-18 enabled SMT solver in Sledgehammer by default
2010-11-18 haftmann 2010-11-18 merged
2010-11-18 haftmann 2010-11-18 keep variables bound
2010-11-18 blanchet 2010-11-18 remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
2010-11-17 haftmann 2010-11-17 merged
2010-11-17 haftmann 2010-11-17 infer variances of user-given mapper operation; proper thm storing
2010-11-17 nipkow 2010-11-17 code eqn for slice was missing; redefined splice with fun
2010-11-17 huffman 2010-11-17 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
2010-11-17 huffman 2010-11-17 merged
2010-11-16 huffman 2010-11-16 typedef (open) unit
2010-11-16 huffman 2010-11-16 add bind_bind rules for powerdomains
2010-11-17 wenzelm 2010-11-17 merged
2010-11-17 haftmann 2010-11-17 emerging Isar command interface
2010-11-17 haftmann 2010-11-17 fixed typo
2010-11-17 haftmann 2010-11-17 updated keywords
2010-11-17 haftmann 2010-11-17 ML signature interface
2010-11-17 haftmann 2010-11-17 stub for Isar command interface
2010-11-17 haftmann 2010-11-17 module for functorial mappers
2010-11-17 wenzelm 2010-11-17 merged
2010-11-17 boehmes 2010-11-17 require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-17 boehmes 2010-11-17 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
2010-11-17 boehmes 2010-11-17 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-16 huffman 2010-11-16 add lemmas about powerdomains
2010-11-16 huffman 2010-11-16 declare {upper,lower,convex}_pd_induct as default induction rules
2010-11-16 huffman 2010-11-16 rename 'repdef' to 'domaindef'
2010-11-17 wenzelm 2010-11-17 refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
2010-11-17 wenzelm 2010-11-17 less parentheses, cf. Session.welcome;
2010-11-16 wenzelm 2010-11-16 avoid spam;
2010-11-16 wenzelm 2010-11-16 more robust determination of java executable;
2010-11-16 wenzelm 2010-11-16 init_component: require absolute path (when invoked by user scripts);
2010-11-16 wenzelm 2010-11-16 more explicit explanation of init_component shell function;
2010-11-16 wenzelm 2010-11-16 paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
2010-11-16 wenzelm 2010-11-16 tuned message;