isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

more position information;

tuned signature;

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;

proper identifiers for consts and types;

eliminated aliases of Type.constraint;

deglobalization

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

discontinued unnamed infix syntax;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

standardized filter/filter_out;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

explicitly qualify Drule.standard;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

modernized Balanced_Tree;

explicit indication of Unsynchronized.ref;

more uniform handling of binding in packages;

cleaned up binding module and related code

eliminated old Sign.read_term/Thm.read_cterm etc.;

pervasive RuleInsts;

RuleInsts.read_instantiate;

Drule.read_instantiate;

moved global pretty/string_of functions from Sign to Syntax;

misc cleanup of embedded ML code;
use more antiquotations;
tuned;

removed unnecessary theory qualifiers;

Made theory names in ZF disjoint from HOL theory names to allow loading both developments
in a single session (but not merge them).

modernized specifications;
removed legacy ML bindings;

avoid unnamed infixes;

BalancedTree;

removed obsolete IFOL.thy/FOL.thy values;

removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);

converted legacy ML scripts;

Term.betapply;

traceIt: plain term;

tuned fold on terms and lists;

Move towards standard functions.

better error messages for datatypes not declared Const

tuned;

use Sign.simple_read_term;

tryres, gen_make_elim moved here;

datatype package improvements

eliminated global/local names;

new inductive, datatype and primrec packages, etc.

mk_all_imp: no longer creates goals that have beta-redexes

Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct

Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML

(co) inductive / datatype package adapted to qualified names;

Replaced map...~~ by ListPair.map

Eta-expansion of a function definition, for value polymorphism

moved ap_split to cartprod.ML

expanded tabs

Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.

intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of
generating a new one. Inductive defs no longer export sumprod_free_SEs

ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM.
It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items
no longer exported.

mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.

data_domain,Codata_domain: removed replicate; now return one
single domain

ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail

ZF/Makefile: now has Inductive.thy,.ML

ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils

replaced Lexicon.scan_id by Scanner.scan_id;
replaced const_name by Syntax.const_name;

ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify

installation of new inductive/datatype sections

removed flatten_typ and replaced add_consts by add_consts_i

removed flatten_term and replaced add_axioms by add_axioms_i

replaced extend_theory by new add_* functions;
changed syntax of datatype declaration

Addition of cardinals and order types, various tidying

Updated refs to old Sign functions

added []-field to extend_theory: no type abbreviations.

ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
ZF/intr-elim/elim_rls: applied make_elim to succ_inject!

ZF/fin: changed type_intrs in inductive def

ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks,
data_elims

ZF/list: now uses datatype_intrs

ZF/ind-syntax/refl_thin: new
ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules

ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac
ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac

ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD
by dresolve_tac InlD,InrD and etac PartE

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext

domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem

ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules

func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new

list/list_case_type: restored!

bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML

nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity

simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss

upair/succ_iff: new, for use with simp_tac (cons_iff already existed)

ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new

ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.

Initial revision