2010-11-30 huffman 2010-11-30 merged
2010-11-30 huffman 2010-11-30 change cpodef-generated cont_Rep rules to cont2cont format
2010-11-30 huffman 2010-11-30 internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
2010-11-30 huffman 2010-11-30 remove gratuitous semicolons from ML code
2010-11-30 huffman 2010-11-30 add continuity lemma for List.map
2010-11-30 huffman 2010-11-30 simplify predomain instances
2010-11-30 boehmes 2010-11-30 merged
2010-11-30 boehmes 2010-11-30 split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models
2010-11-30 haftmann 2010-11-30 code preprocessor setup for numerals on word type; less meta-equalites; more xsymbols; less implicit propositions
2010-11-30 haftmann 2010-11-30 merged
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy
2010-11-30 haftmann 2010-11-30 adapted fragile proof
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy
2010-11-30 haftmann 2010-11-30 merged
2010-11-30 haftmann 2010-11-30 more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-30 haftmann 2010-11-30 adapted proofs to slightly changed definitions of congruent(2)
2010-11-29 haftmann 2010-11-29 reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent2 by plain definition
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent by plain definition
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
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