isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

isabelle update_inner_syntax_cartouches;

embedded content may be delimited via cartouches;

isabelle update_cartouches -c -t;

more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;

isabelle update_cartouches;

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

tuned;

local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

support 'for' fixes in rule_tac etc.;

tuned signature;

more position information;

proper context for match_tac etc.;

modernized header uniformly as section;

modernized setup;

tuned signature;

tuned import;

uniform Proof.context for hyp_subst_tac;

simplifier uses proper Proof.context instead of historic type simpset;

discontinued obsolete ML antiquotation @{claset};

prefer ML_file over old uses;

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

declare command keywords via theory header, including strict checking outside Pure;

more antiquotations;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned;

ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

simplified/unified method_setup/attribute_setup;

simplified BLAST_DATA;

modernized functor names;
tuned;

clarified map_simpset versus Simplifier.map_simpset_global;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

simplified Blast setup;

misc tuning and simplification;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;

modernized Quantifier1 simproc setup;

clarified simpset setup;
discontinued unused old-style FOL_css;

setup case_product attribute in HOL and FOL

modernized specifications;

proper identifiers for consts and types;

modernized specifications;

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

Adapted to changes in setup of cases method.

Adapted to changes in setup of induct method.

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

removed old global get_claset/map_claset;
added local get_claset/put_claset;

renamed functor BlastFun to Blast, require explicit theory;
eliminated src/FOL/blastdata.ML;

renamed functor InductFun to Induct;

removed obsolete CVS Ids;

simplified method setup;

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.

Args.name_source(_position) for proper position information;

tuned document;

pervasive RuleInsts;

removed unused excluded_middle_tac;
proper context for tactics derived from res_inst_tac;
tuned setup;

eliminated obsolete case_split_thm -- use case_split;

purely functional setup of claset/simpset/clasimpset;

pass imp_elim, swap to classical prover;

added lemmas from simpdata.ML;

moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;

moved classical tools from theory IFOL to FOL;

tuned header;

tuned ML setup;

converted legacy ML scripts;

tuned proofs;

tuned proofs;

simplified EqSubst setup;

tuned EqSubst setup;

removed obsolete cla_dist_concl;

provide cla_dist_concl;

removed obsolete induct_atomize_old;

updated auxiliary facts for induct method;

migrated theory headers to new format

the new subst tactic, by Lucas Dixon

removed obsolete dependency;

new case_tac method

moved some lemmas here from ZF

removal of blast.overloaded

removed declaration of disjI1, disjI2 (already done in IFOL);

tuned;

induct method: localize rews for rule;

induct_atomize: include atomize_conj (for mutual induction);

val local_imp_def = thm "induct_implies_def";

theorems case_split = case_split_thm [case_names True False, cases type: o];

induct_impliesI;

calculational rules moved from FOL to IFOL;

moved rulify to ObjectLogic;

moved atomize stuff to theory IFOL;
added induct/cases setup;

tuned trans rules;

added atomize_eq;

"atomize" for classical tactics;

added == transitive rule (bad idea??);

setup Rulify.setup;

cong setup now part of Simplifier;

lemmas atomize = all_eq imp_eq;

improved comments;
added all_eq, imp_eq (for blast);
basic calculational rules;

added cong atts;

splitter setup;

proper bootstrap of IFOL/FOL theories and packages;

attrib_setup;

tuned setup;

replaced thy_data by thy_setup;

added claset thy_data;

Initial revision