2009-12-17 huffman 2009-12-17 added lemmas about INFM/MOST
2009-12-17 huffman 2009-12-17 add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
2009-11-29 huffman 2009-11-29 add lemmas open_image_fst, open_image_snd
2009-12-17 wenzelm 2009-12-17 Result.cache;
2009-12-17 wenzelm 2009-12-17 cache for partial sharing;
2009-12-17 wenzelm 2009-12-17 merged
2009-12-17 paulson 2009-12-17 Two new theorems about cardinality
2009-11-23 huffman 2009-11-23 replace 'UNIV - S' with '- S'
2009-11-24 huffman 2009-11-24 re-state lemmas using 'range'
2009-11-29 huffman 2009-11-29 make proof use only abstract properties of eventually
2009-12-16 huffman 2009-12-16 swap_self already declared [simp]
2009-12-16 huffman 2009-12-16 declare swap_self [simp], add lemma comp_swap
2009-12-17 wenzelm 2009-12-17 fifo: raw byte stream; Result: fully decoded symbols and tree structure; adapted to simplified message format; tuned;
2009-12-17 wenzelm 2009-12-17 added decode_chars, with raw character view on byte buffer and adhoc decoding via toString; parse/chunks: avoid direct string comparison, to make it actually work with abstract CharSequence;
2009-12-17 wenzelm 2009-12-17 tuned signature;
2009-12-17 wenzelm 2009-12-17 tuned;
2009-12-17 wenzelm 2009-12-17 simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;
2009-12-17 wenzelm 2009-12-17 robust representation of low ASCII control characters within XML/YXML text;
2009-12-16 wenzelm 2009-12-16 merged
2009-12-16 wenzelm 2009-12-16 filter out identical completions;
2009-12-16 haftmann 2009-12-16 spaces not allowed, unfortunately
2009-12-16 haftmann 2009-12-16 user aliasses
2009-12-14 boehmes 2009-12-14 merged
2009-12-14 boehmes 2009-12-14 replaced blast by metis (blast hangs with polyml-5.2)
2009-12-14 haftmann 2009-12-14 avoid negative indices as argument ot drop
2009-12-14 paulson 2009-12-14 Upgraded a warning to an error
2009-12-14 haftmann 2009-12-14 merged
2009-12-14 haftmann 2009-12-14 improved crude deriving_show inference
2009-12-14 haftmann 2009-12-14 explicit name for function space
2009-12-14 blanchet 2009-12-14 make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
2009-12-14 blanchet 2009-12-14 make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
2009-12-14 haftmann 2009-12-14 made sml/nj happy
2009-12-14 boehmes 2009-12-14 also sort verification conditions before printing
2009-12-13 boehmes 2009-12-13 print assertions in a more natural order
2009-12-11 wenzelm 2009-12-11 removed unique ids -- now in session.scala;
2009-12-11 wenzelm 2009-12-11 merged
2009-12-11 wenzelm 2009-12-11 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;
2009-12-11 wenzelm 2009-12-11 Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
2009-12-11 haftmann 2009-12-11 merged
2009-12-11 haftmann 2009-12-11 repaired accident: do not forget module contents if there are no imports
2009-12-11 haftmann 2009-12-11 option width for Code_Target.code_of
2009-12-11 haftmann 2009-12-11 default_code_width is now proper theory data
2009-12-11 boehmes 2009-12-11 merged
2009-12-11 boehmes 2009-12-11 updated dependencies
2009-12-11 boehmes 2009-12-11 make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations
2009-12-11 boehmes 2009-12-11 depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
2009-12-11 haftmann 2009-12-11 merged
2009-12-11 haftmann 2009-12-11 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-12-11 haftmann 2009-12-11 avoid dependency on implicit dest rule predicate1D in proofs
2009-12-11 haftmann 2009-12-11 merged
2009-12-11 haftmann 2009-12-11 NEWS
2009-12-11 haftmann 2009-12-11 merged
2009-12-09 haftmann 2009-12-09 merged
2009-12-09 haftmann 2009-12-09 take and drop as projections of chop
2009-12-09 haftmann 2009-12-09 explicit lower bound for index
2009-12-11 paulson 2009-12-11 merged
2009-12-10 paulson 2009-12-10 merged
2009-12-10 paulson 2009-12-10 streamlined proofs
2009-12-10 paulson 2009-12-10 fixed typo
2009-12-10 wenzelm 2009-12-10 merged