eliminate constant 'coerce'; use 'prj oo emb' instead

simplify fixrec pattern match function

simplify some proofs

tuned

added some facts about factorial and dvd, div and mod

removing something that probably slipped into the Quotient_List theory

Quotient package: partial equivalence introduction

reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)

remove dead code

remove old uses of 'simp_tac HOLCF_ss'

merged

remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check

reimplement proof automation for coinduct rules

add functions mk_imp, mk_all

move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code

simplify automation of induct proof

add function mk_adm

rewrite proof automation for finite_ind; get rid of case_UU_tac

put constructor argument specs in constr_info type

avoid using Global_Theory.get_thm

include iso_info as part of constr_info type

remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors

add take_strict_thms field to take_info type

add record type synonym 'constr_info'

add function take_theorems

add type annotation to avoid warning

cleaned up Fun_Cpo.thy; deprecated a few theorem names

edit comments

remove unneeded lemmas Lift_exhaust, Lift_cases

move lemmas from Lift.thy to Cfun.thy

cleaned up Adm.thy

remove unneeded lemmas from Fun_Cpo.thy

remove unused lemmas

reformulate lemma cont2cont_lub and move to Cont.thy

remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2

new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI

rename Ffun.thy to Fun_Cpo.thy

remove unused constant 'directed'

add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite

merged

prevention of self-referential type environments

FSet: definition changes propagated from Nominal and more use of 'descending' tactic

FSet tuned

FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash

NEWS

removed output syntax "'a ~=> 'b" for "'a => 'b option"

reactivated

slightly more robust proof

renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)

merged

move all bifinite class instances to Bifinite.thy

rename class 'sfp' to 'bifinite'

move stuff from Algebraic.thy to Bifinite.thy and elsewhere

add lemma typedef_ideal_completion

remove unused lemmas

remove Infinite_Set from ROOT.ML

remove some junk that made it in by accient

"setup" in theory

added "trace_meson" configuration option, replacing old-fashioned reference

added "trace_metis" configuration option, replacing old-fashioned references

do not mention unqualified names, now that 'global' and 'local' are gone

simplified proof

avoid generating several formulas with the same name ("tfrees")

major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);

add lemma finite_deflation_intro

add lemmas finite_deflation_imp_compact, cast_below_cast_iff

move lemmas to Deflation.thy

simplify proofs of powerdomain inequalities

new lemmas about lub

define is_ub predicate using bounded quantifier

minimize theory imports

added lemmas to List_Cpo.thy

new_domain emits proper error message when a constructor argument type does not have sort 'rep'

move code from "Metis_Tactics" to "Metis_Reconstruct"

merged

qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)

get rid of function that duplicates existing Pure functionality

remove needless fact

added a few FIXMEs

tuned comments

document latest changes to Meson/Metis/Sledgehammer

remove needless Metis facts

hide one more name

qualify names

hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names

clean up debugging output

factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

got rid of overkill "meson_choice" attribute; tuning

more explicit name

factor out "Meson_Tactic" from "Meson_Clausify"

tuning

move Metis into Plain

added "Meson" theory to Makefile

update authors

remove Meson from Hilbert_Choice

remove Meson from Sledgehammer

move Meson to Plain

move MESON files together

paramify new skolems just like old ones (cf. reveal_old_skolem_terms)

fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset

correctly handle multiple copies of the same axiom with the same types

put two operations in the right order

reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism

apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed

instantiate foralls and release exists in the order described by the topological order

reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables

renamed internal function

hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving

tuned header

tuned

force less agressively

lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed

removed complicated (and rarely helpful) error reporting

discontinued continuations to simplify control flow; dropped optimization in scnp

use Cache structure instead of passing tables around explicitly

merged

lemmas fold_commute and fold_commute_apply

spelling

adjusted to inductive characterization of sorted

tuned whitespace

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

turned distinct and sorted into inductive predicates: yields nice induction principles for free

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

some Poly/ML-specific debugging code escaped in the wild -- comment it out

merged

avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime

moved ML_Context.value to Code_Runtime

constant `contents` renamed to `the_elem`

merged

tune whitespace

rename bound variables after skolemizing, if the axiom of choice is available

tuning

rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)

tune bound names

merged

avoid dependency on "int"

make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice

added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice

compute quantifier dependency graph in new skolemizer

tuning

compute substitutions in new skolemizer

encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions

reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer

encode number of skolem assumptions in them, for more efficient retrieval later

move functions closer to where they're used

Skolemizer tweaking

"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))

finished renaming file and module

rename file

ignore Skolem assumption (if any)

second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions

first step towards a new skolemizer that doesn't require "Eps"

cumulative update of generated files (since bf164c153d10);

removed ML_old.thy, which is largely superseded by ML.thy;

more on "Canonical argument order"; tuned;

cover @{Isar.state};

more on "Style and orthography";

more on "Naming conventions"; tuned;

tuned;

more on "Style and orthography";

more refs;

preliminary material on "Concrete syntax and type-checking";

more on "Association lists", based on more succinct version of older material;

clarified "lists as a set-like container";

more robust treatment of "op IDENT";

more on messages;

more on synchronized variables;

tuned;

more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);

misc tuning;

somewhat modernized version of "Thread-safe programming";

more robust examples: explicit @{assert} instead of unchecked output;

more on "Configuration options";

tuned;

more on "Basic data types"; tuned;

more on "Integers";

use continental paragraph style, which works better with mixture of (in)formal text; tuned skips and indents; tuned;

robustified "warn" environment if \parindent is zero (e.g. within itemize, description etc.);

more on "Basic ML data types";

more robust treatment of symbolic indentifiers (which may contain colons);

more examples;

tuned;

more on "Exceptions"; tuned;

more on "Exceptions";

more examples;

tuned chapter arrangement;

more examples; tuned;

moved bind_thm(s) to implementation manual;

more on "Attributes"; tuned;

misc tuning and clarification;

more on "Proof methods"; more examples; tuned;

examples in Isabelle/HOL; tuned;

more on Proof.theorem;

tuned;

more examples; more on "Proof methods";

more on "Isar language elements";

more examples;

more refs;

misc tuning;

removed some obsolete reference material;

cover some more theory operations;

note on Isabelle file specifications; removed junk;

modernized version of "Message output channels";

removed some really old reference material;

more examples;

various concrete ML antiquotations;

prefer checked antiquotations;

clarified tag markup;

more on ML antiquotations; tuned;

keep normal size for %mlref tag;

basic setup for ML antiquotations -- with rail diagrams; tuned;

eliminated "Toplevel control", which belongs to TTY/ProofGeneral model;

eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX); eliminated Isar toplevel invocation functions, which belong to TTY/ProofGeneral model; moved remaining "ML toplevel" material to "Compile-time context";

misc tuning;

more on Isabelle/ML;

basic setup for Chapter 0: Isabelle/ML;

minor tuning and updating;

made SML/NJ happy;

merged

use module integer for Eval

check whole target hierarchy for existing reserved symbols

added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!

tuned default "Prover Session" perspective;

eliminated ancient OldTerm.term_frees;

more antiquotations;

simplified outer syntax setup; slightly more uniform Isabelle/ML indentation style;

chop_while replace drop_while and take_while

merged

take_while, drop_while

rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs

fixrec: rename match_cpair to match_Pair

remove code for obsolete 'fixpat' command

clean up definition of compile_pat function

rename some fixrec pattern-match compilation functions

adding example for case expressions

applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux

merged

adapting manual configuration in examples

finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)

adding option to globally limit the prolog execution