set_preproc for object-logics with type classes;

purge remains from test (cf. 5a53724fe247);

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update_inner_syntax_cartouches;

isabelle update -u mixfix_cartouches;

support named ML environments, notably "Isabelle", "SML";
more uniform options ML_read_global, ML_write_global;
clarified bootstrap environment;

repair LaTeX dropout from f83ef97d8d7d

more symbols;

isabelle update_cartouches -c -t;

repaired document;

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

discontinued specific HTML syntax;

isabelle update_cartouches;

proper context and method setup;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

proper context for assume_tac (atac remains as fall-back without context);

modernized header uniformly as section;

modernized setup;

modernized module name and setup;

prefer vacuous definitional type classes over axiomatic ones;

tuned import;

standardized aliases;

uniform Proof.context for hyp_subst_tac;

eliminated some old material that is unused in the visible universe;

prefer ML_file over old uses;

modernized axiomatization;
eliminated odd 'finalconsts';

old term operations are legacy;

modernized functor names;
tuned;

tuned;

modernized specifications;

proper identifiers for consts and types;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

more antiquotations;

deglobalization

renamed command 'defaultsort' to 'default_sort';

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

more antiquotations;
eliminated legacy ML bindings;

modernized some syntax translations;

modernized structure Context_Rules;

renamed functor ProjectRuleFun to Project_Rule;
renamed structure ProjectRule to Project_Rule;

modernized method setup;

Merge.

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;

--HG--
rename : src/Provers/coherent.ML => src/Tools/coherent.ML
rename : src/Provers/eqsubst.ML => src/Tools/eqsubst.ML
rename : src/Provers/project_rule.ML => src/Tools/project_rule.ML

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

Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.

subst is a proper axiom again

removed obsolete/unused pred_congs;

tuned comments;

setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic

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 proofs: avoid implicit prems;

moved IsaPlanner from Provers to Tools;

proper loading of ML files;

tuned proofs;

tuned ML setup;

converted legacy ML scripts;

updated (binder) syntax/notation;

more robust syntax for definition/abbreviation/notation;

renamed 'const_syntax' to 'notation';

lemmas strip;

removed obsolete 'finalconsts';

tuned concrete syntax -- abbreviation/const_syntax;

tuned syntax/abbreviations;

refined 'abbreviation';

not_equal: replaced syntax translation by abbreviation;
simplified Pure conjunction;

declare defn rules;

added atomize_iff;

setup: theory -> theory;

fixed final_consts;

structure ProjectRule;

more finalconsts;

renamed rules to iprover

avoid old-style infixes;

migrated theory headers to new format

tuned;

Simplifier already setup in Pure;

the new subst tactic, by Lucas Dixon

proof of subst by S Merz

removed obsolete sort 'logic';

use more symbols in HTML output

partial conversion to Isar scripts

moving "let" from ZF to FOL

new theorem eq_commute

clarified syntax of ``long'' statements: fixes/assumes/shows;

tuned;

syntax "_not_equal";

sym declarations;
tuned declarations;

renamed RuleContext to ContextRules;

setup "rules" method;

eliminated old "symbols" syntax, use "xsymbols" instead;

transitive declared in Pure;

equal_intr_rule already declared in Pure;

atomize_conj;

calculational rules moved from FOL to IFOL;

moved rulify to ObjectLogic;

judgment Trueprop;
proper declarations of atomize rules;

declare impE iffD1 iffD2 ad elim of Pure;

atomize stuff from theory FOL;
tuned;

updated setup;

setup hypsubst_setup;

proper bootstrap of IFOL/FOL theories and packages;

HTML output;

added new print_mode "xsymbols" for extended symbol support
(e.g. genuiely long arrows)

tuned setup;

replaced thy_data by thy_setup;

added simpset thy_data;

local;

global;

fixed dots;

fixed pris of binder syntax;

symbol names changes;

added symbolfont syntax;

removed quotes from types in consts section

corrected title

Moved declaration of ~= to a syntax section

adapted type definition to new syntax

added white-space;
made ~= a fake infix;

ifol.thy: added ~= for "not equals"

Initial revision