2010-11-29 haftmann 2010-11-29 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules
2010-11-29 haftmann 2010-11-29 moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules
2010-11-29 haftmann 2010-11-29 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition
2010-11-30 huffman 2010-11-30 simplify proof of LIMSEQ_unique
2010-11-30 huffman 2010-11-30 use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-11-30 huffman 2010-11-30 merged
2010-11-29 huffman 2010-11-29 instance list :: (discrete_cpo) discrete_cpo; compactness lemmas for Nil, Cons; instance list :: (chfin) chfin;
2010-11-30 boehmes 2010-11-30 merged
2010-11-29 boehmes 2010-11-29 also support higher-order rules for Z3 proof reconstruction
2010-11-29 wenzelm 2010-11-29 merged
2010-11-29 haftmann 2010-11-29 less ghc-specific pragma
2010-11-29 haftmann 2010-11-29 tuned
2010-11-29 wenzelm 2010-11-29 updated generated files;
2010-11-29 wenzelm 2010-11-29 added document antiquotation @{file};
2010-11-28 wenzelm 2010-11-28 Parse.liberal_name for document antiquotations and attributes;
2010-11-28 wenzelm 2010-11-28 ML results: enter before printing (cf. Poly/ML SVN 1218);
2010-11-28 wenzelm 2010-11-28 merged
2010-11-28 huffman 2010-11-28 merged
2010-11-28 huffman 2010-11-28 merged
2010-11-28 huffman 2010-11-28 change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec
2010-11-27 huffman 2010-11-27 add lemma cont2cont_if_bottom
2010-11-28 wenzelm 2010-11-28 added Parse.literal_fact with proper inner_syntax markup (source position); tuned;
2010-11-28 wenzelm 2010-11-28 tuned signature;
2010-11-28 wenzelm 2010-11-28 less frequent sidekick parsing, which is relatively slow;
2010-11-28 wenzelm 2010-11-28 basic setup for bundled Java runtime;
2010-11-28 wenzelm 2010-11-28 updated reference platforms;
2010-11-28 wenzelm 2010-11-28 merged
2010-11-28 nipkow 2010-11-28 merged
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-11-28 wenzelm 2010-11-28 more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);
2010-11-28 wenzelm 2010-11-28 added 'syntax_declaration' command;
2010-11-28 wenzelm 2010-11-28 more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
2010-11-28 wenzelm 2010-11-28 superficial tuning;
2010-11-28 wenzelm 2010-11-28 updated versions;
2010-11-28 wenzelm 2010-11-28 recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-28 wenzelm 2010-11-28 follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);
2010-11-28 krauss 2010-11-28 removed HOLCF for now as explicit component
2010-11-27 huffman 2010-11-27 fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-27 huffman 2010-11-27 update web description of HOLCF; fix broken link to HOLCF/index.html
2010-11-27 huffman 2010-11-27 remove HOLCF from build script, since it no longer works
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;
2010-11-27 huffman 2010-11-27 merged
2010-11-27 huffman 2010-11-27 rename Pcpodef.thy to Cpodef.thy; rename pcpodef.ML to cpodef.ML;
2010-11-27 huffman 2010-11-27 renamed several HOLCF theorems (listed in NEWS)
2010-11-27 huffman 2010-11-27 rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
2010-11-27 huffman 2010-11-27 rename rep_contlub lemmas to rep_lub
2010-11-27 huffman 2010-11-27 rename function 'match_UU' to 'match_bottom'
2010-11-27 huffman 2010-11-27 rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 corrected: use canonical variables of type scheme uniformly
2010-11-27 haftmann 2010-11-27 tuned
2010-11-26 haftmann 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings
2010-11-26 haftmann 2010-11-26 tuned example
2010-11-27 wenzelm 2010-11-27 merged
2010-11-27 haftmann 2010-11-27 updated generated documents