merged

change cpodef-generated cont_Rep rules to cont2cont format

internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules

remove gratuitous semicolons from ML code

add continuity lemma for List.map

simplify predomain instances

merged

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

code preprocessor setup for numerals on word type; less meta-equalites; more xsymbols; less implicit propositions

merged

adaptions to changes in Equiv_Relation.thy

adapted fragile proof

adaptions to changes in Equiv_Relation.thy; prefer primrec if possible

adaptions to changes in Equiv_Relation.thy

merged

more systematic and compact proofs on type relation operators using natural deduction rules

adapted proofs to slightly changed definitions of congruent(2)

reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text

replaced slightly odd locale congruent2 by plain definition

replaced slightly odd locale congruent by plain definition

equivI has replaced equiv.intro

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

moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition

simplify proof of LIMSEQ_unique

use new 'file' antiquotation for reference to Dedekind_Real.thy

merged

instance list :: (discrete_cpo) discrete_cpo; compactness lemmas for Nil, Cons; instance list :: (chfin) chfin;

merged

also support higher-order rules for Z3 proof reconstruction

merged

less ghc-specific pragma

tuned

updated generated files;

added document antiquotation @{file};

Parse.liberal_name for document antiquotations and attributes;

ML results: enter before printing (cf. Poly/ML SVN 1218);

merged

merged

merged

change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec

add lemma cont2cont_if_bottom

added Parse.literal_fact with proper inner_syntax markup (source position); tuned;

tuned signature;

less frequent sidekick parsing, which is relatively slow;

basic setup for bundled Java runtime;

updated reference platforms;

merged

merged

gave more standard finite set rules simp and intro attribute

more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);

added 'syntax_declaration' command;

more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;

superficial tuning;

updated versions;

recovered Isabelle2009-2 NEWS -- published part is read-only;

follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);

removed HOLCF for now as explicit component

fix cut-and-paste errors for HOLCF entries in IsaMakefile

update web description of HOLCF; fix broken link to HOLCF/index.html