NameSpace.is_qualified;

Pretty.chunks;

mod to error msg

next_block: reset_facts;

plain ASCII;

intrn_arity: reject type abbreviations;

added is_type_abbr;

\newenvironment{isabellequote};

global \isa@parindent, \isa@parskip; \newcommand{\isa};

use HOLogic.termT;

outer syntax: no simps;

recdef: no simps;

stopped using the obsolete "nat_ind_tac"

added some new iff-lemmas; removed some obsolete thms

tidied

tuned;

*** empty log message ***

Simplifier options;

Times -> <*> ** -> <*lex*>

fixed ??/?;

fixed index;

added simp_options; removed emulations of simp_tac etc.;

intro/elim_tac: match only;

made mod_less_divisor a simplification rule.

InductMethod.concls_of;

tuned;

export concl_of; induct method: admit "_";

tuned \isasymlbrace;

'insts' syntax; 'insert' method;

improved 'induct(_tac)' syntax;

added 'insert' method;

added inst, insts;

improved induct_tac;

induct stripped: match_tac;

Args.name_dummy;

fixed 'induct_tac' syntax;

handle dir prefix;

improved document preparation;

fixed comment;

added 'ML_command'; 'apply' etc.: comments;

apply etc.: comments;

tuned \isasymlbrace;

added \isasymlbrace, \isasymrbrace, \isasymtop;

'welcome' made diagnostic;

added Isar_examples/NestedDatatype.thy;

added NestedDatatype.thy;

added NestedDatatype;

fixed goal selection;

Isar: simplified (more robust) goal selection of proof methods; Isar: tuned 'let' syntax: replace 'as' keyword by 'and';

induct/case_tac emulation: optional rule; add_cases_induct: fixed case names;

HEADGOAL;

tuned comment;

removed "as" keyword;

suppress warning;

print_simpset / print_claset command;

case_tac / induct_tac: optional rule;