simplified HOL.eq simproc matching;

tuned;

just one Term.dest_funT;

activate subtyping/coercions in theory Complex_Main;

simplified equality on pairs of types;

more precise dependencies;

two-staged architecture for subtyping; improved error messages of subtyping (using the new architecture); bugfix: constraint graph consistency check after cycle elimination;

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

remove HOLCF from build script, since it no longer works

moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;

merged

rename Pcpodef.thy to Cpodef.thy; rename pcpodef.ML to cpodef.ML;

renamed several HOLCF theorems (listed in NEWS)

rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo

rename rep_contlub lemmas to rep_lub

rename function 'match_UU' to 'match_bottom'

rename function 'strict' to 'seq', which is its name in Haskell

merged

merged

typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned

merged

merged

corrected: use canonical variables of type scheme uniformly

tuned

merged

consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings

tuned example

merged

updated generated documents

added equation for Queue; tuned proofs

added evaluation section

tuned formatting; adjustments to changes on ML level

added label

more thorough process termination (cf. Scala version);

prefer Isabelle/ML concurrency elements; more careful propagation of interrupts;

removed bash from ML system bootstrap, and past the Secure ML barrier;

more proper int wrappers;

explicit check for requirement;

more basic Isabelle_System.mkdir;

tuned;

more explicit Isabelle_System operations;

prefer Synchronized.var over CRITICAL/Unsynchronized.ref;

moved file identification to thy_load.ML (where it is actually used);

removed some old settings;

recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);

merged

remove map function names from domain package theory data

isar-style proof for lemma contI2

remove case combinator for fixrec match type

declare more simp rules for powerdomains

merged; adapted ListPair.UnequalLengths;

merged

strict forall2

nbe decides equality of abstractions by extensionality

eliminated some generated comments;

merged

merged

keep type variable arguments of datatype constructors in bookkeeping

document changes in Nitpick and MESON/Metis

renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs