unfold intermediate (internal) pred definitions

formal position for PThm nodes;

isabelle update -u control_cartouches;

smash position to avoid position of other file "~~/src/HOL/BNF_Composition.thy" (due to "bnf ID"), e.g. relevant for "HOL-Nominal-Examples.Class1";

more symbols;

tuned signature

provide a mechanism for ensuring dead type variables occur in typedef if desired

preserve order of dead variables

tuning

generalized ML signature

extended ML signature

document that n2m does not depend on most things in fp_sugar in its type

generalized ML function

make predicator a first-class bnf citizen

use 'undefined' instead of 'Eps'

tuned whitespace

congruence rules for the relator

prefer tactics with explicit context;

prefer tactics with explicit context;

{r,e,d,f}tac with proper context in BNF

renamed misleading option

removed TODO

tuned signature;

preserve order of type arguments in pre-FP BNF typedef

register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

tuning

export more ML functions

inlining threshold

respect order of deads when retrieving bnfs from the database

renamed "pairself" to "apply2", in accordance to @{apply 2};

allow sorts on dead variables in BNFs

proper proof context for typedef;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')

imported patch phantoms

new deads go to the end

renamed internal constant

renamed BNF theories

--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy

use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)

use the noted theorems in 'BNF_Comp'

add mk_Trueprop_mem utility function

tuned whitespace

more antiquotations;

copy-paste typo

unfold intermediate definitions after sealing the bnf

more careful unfolding of internal constants

made typedef for the type of the bound optional (size-based)

removed junk

tuned

move special BNFs used for composition only to BNF_Comp;
use local copy of identity function that gets unfolded later for ID

more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms

no 'sorry' so that the schematic variable gets instantiated

simplify sets in BNF composition

more caching in composition pipeline

propagate the exception that is expected later on

got rid of automatically generated fold constant and theorems (to reduce overhead)

use same identity function for abs and rep (doesn't seem to confuse any proofs)

make 'typedef' optional, depending on size of original type

use aconv to compare terms (for cleanliness)

optimize cardinal bounds involving natLeq (omega)

joint work with blanchet: intermediate typedef for the input to fp-operations

clarified interaction with dead variables in the composition of BNFs

added BNF cache (within one definition)

updated docs

optimized 'bnf_of_typ' further w.r.t. dead variables

optimization of 'bnf_of_typ' if all variables are dead

allow different functions to recurse on the same type, like in the old package

less hermetic tactics

tuned names

adjusted comments

avoid nested 'Tools' directories

--HG--
rename : src/HOL/Tools/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/bnf_comp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/bnf_comp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/bnf_def.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/bnf_def_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/bnf_fp_n2m.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/bnf_fp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/bnf_gfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/bnf_gfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/bnf_lfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/bnf_lfp_compat.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/bnf_lfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/bnf_lfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/bnf_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/bnf_util.ML