named code theorem for Fract_norm

tuned settings;

merged

removed references to OldTerm.*

tuned message_text;

removed obsolete XML mode; tuned comments; tuned;

xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;

Markup.no_output;

added output; improved encode_raw: map empty to empty; tuned;

removed unused add_substring; back to simple list implementation;

renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;

removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;

updated rendering of inner token markup;

more detailed inner token markup;

added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;

renamed token markup "_xstr" to "_inner_string";

removed dead code; proper "_numeral" token markup; proper printing of arguments (higher-order numerals);

renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);

tuned;

Isar.command: plain Position.id; tuned;

added type 'a parser, simplified signature;

added type 'a parser, simplified signature; added internal_command wrapper; tuned;

added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;

added props_text (from outer_parse.ML);

added Isar/value_parse.ML: Outer syntax parsers for basic ML values.

added id; tuned;

MetaSimplifier.SIMPLIFIER;

fixed assumption proof;

tuned header and description of boot files;

merged;

normalized some ML type/val aliases;

assumption/close: discontinued implicit prems;

avoid implicit use of prems;

updated generated files;

eliminated implicit use of prems; unified fact names: a, b, ab;

updated generated files;

updated type 'a lazy; proper name for type simpset;

proper import of ~~/src/HOL/ex/ReflectedFerrack;

crude adaption to intermediate class/locale version;

crude adaption to new locales;

avoid implicit prems -- tuned proofs;

avoid implicit use of prems;

Term.add_consts;

eliminated OldTerm.(add_)term_consts; eliminated polymorphic version of insert;

avoid polymorphic equality;

eliminated OldTerm.(add_)term_consts;

added canonical add_const_names, add_consts;

provide structure CharVector;

isabelle-process; provide structure Word; provide IntInf.log2;

updated sessions;

removed unused add_term_free_names;

eliminated OldTerm.add_term_free_names;

updated header;

Term.declare_typ_names, Term.declare_term_frees;

added declare_term_frees; tuned signature;

Term.declare_term_frees;

qualified Term.rename_wrt_term;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;

use fold_aterms directly;

use exists_Const directly;

use regular Term.add_XXX etc.;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;

use exists_subterm directly; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use exists_subterm directly;

use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use regular Term.add_vars, Term.add_frees etc.;

added old_term.ML;

Some old-style term operations.

freeze_thaw: canonical Term.add_XXX operations; varify: regular name context;

varify: regular name context;

canonical Term.add_var_names, Term.add_tvar_namesT;

canonical Term.add_var_names;

provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names; renamed add_varnames to add_var_names; removed old add_typ_ixns, add_term_tvar_ixns;

removed unused head_name_of; tuned;

merged

prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;

New locales.

Merged.

Temporarily avoid type errors in parse phase.

More liberal consistency check for defines elements.

All logics ported to new locales.

Merged.

adapted statespace module to new locales;

More porting to new locales.

Intro_locales_tac knows about defines elements; more robust export morphism.

More porting to new locales.

Merged.

More porting to new locales

Merged.

More porting to new locales.

Prevent defines from being checked in interpretation.

Merged.

More porting to new locales.

Merged.

More porting to new locales.

More porting to new locales.

Ported HOL and HOL-Library to new locales.

Fixed legacy locale keywords (went to ZF rather than default keywords file).

Merged.

Merged.

Porting to new locales.

Theory target distinguishes old and new locales.

Merged.

Ported to new locales.

Merged; updated interpretation command in isar_syn.ML.

Merged.

Conversion of HOL-Main and ZF to new locales.

Add inherited registrations.

Refactored: evaluate specification text only in locale declarations.