eliminated rulify setup (now in Provers/rulify.ML);

tuned msg;

updated rulify setup;

added Provers/rulify;

removed rulify_attrib_setup;

rulify setup;

added Provers/rulify.ML;

eliminated rulify stuff (now in Provers/rulify.ML);

updated setup;

setup Rulify.setup;

Conversion of object-level -->/ALL into meta-level ==>/!!;

a number of new theorems

Added meaningful output to cong-error msg.

strengthened dvd_mod & proofed dvd_mod_iff

tuned;

make SML/NJ happy;

fixed structure U;

less_induct -> nat_less_induct

tuned;

imp_cong bound at thm level.

bug fix for arithmetic simprocs (nat & int)

tidied

new Iff theorem zero_le_succ_iff

*** empty log message ***

less_induct -> nat_less_induct

improved meson setup;

fixed quotes;

tuned;

proper handling of hints; tuned;

eliminated;

generalized types of args;

tuned output of isabelle env;

improved add_rules;

removed 'other' modifier;

added 'iff' declarations;

recdef hints (attributes and modifiers);

use 'iff' modifier;

RecdefPackage.add_recdef_old;

added not_const;

improved recdef setup;

lemmas [recdef_cong] = map_cong;

removed Add_recdef_congs [map_cong] (see Main.thy);

tuned setup;

iff declarations moved to clasimp.ML;

added not;

simplified PG/X-Symbol intro;

recdef hints (attributes and modifiers); improved rails;

added 'iff' modifier; removed 'other' modifier;

tuned;

updated;

*** empty log message ***

tidied, proving gcd_greatest_iff and using induct_tac

new AddIffs (especially Memrel_iff)

safe_meson_tac -> meson_tac

meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default

loads Tools/meson.ML: meson_tac installed by default

moved proof of "choice" to Tools/meson.ML

fixed a slow proof

simplified two index entries, since now ZF is by itself

meson_tac

*** empty log message ***

tuned comment;

added safe_mk_meta_eq;

tuned "mono" att setup;

tuned;

added add_rules, del_rules;

display: avoid empty lines;

tuned;

minor fixes for new version of Primes.thy

Renamed real_of_posnat_less_zero to real_of_posnat_gt_zero

Converting HOL/ex/Primes.thy to new style, removing Primes.ML

BCV

added pretend_use_thy_only;

proper_inform_file_processed: ThyInfo.pretend_use_thy_only;

improved section markup;

tuned;

GPLed;

GPLed; show targets;

new reference girard89

Lambda/document/root.tex;

* HOL/Lambda: converted into new-style theory and document;

document setup;

updated;

HOL/Lambda: converted into new-style theory and document;

method_setup: thms closure;

added mode parser;

added get_thm_closure;

"split": added "(asm)" option;

added "slow";

added "slowsimp", "bestsimp";

"inductive_cases": proper command;

use Args.mode;

converted;

added 'iff del' att;

tuned rail;

'split' method: '(asm)' option; added 'slow', 'slowsimp', 'bestsimp' methods;

some stuff;

provide "--" argument: tentative release; tuned;

tuned;

copy_files: do not quote paths (for now);

fixed quoting;

isatool nonascii;

*** empty log message ***

Completely new version of BCV

ISABELLE_PATH: ML_IDENTIFIER no longer added; tuned;

GPLed; more robust handling of spaces in args / file names;

GPLed; more robust handling of spaces in args / file names;

more robust handling of spaces in args / file names; tuned;

GPLed; more robust handling of spaces in args / file names; tuned;

isatool_document: quote args;

export quote_sysify_path;

/usr/bin/perl;

cleanup dist sources afterwards; tmp version;

cvs-copy - make copy of CVS controlled directory hierarchy;

added 'safe' method; 'auto' method: optional parms;

Method.bang_sectioned_args';

replaced writeln by priority;

added bang_sectioned_args';

'declare' made proper command;

priority_fn := decorate_lines; replaced 'message' by 'priority';

added priority, priority_fn;

added "safe" method;

auto method: opt args; tuned;

converted Lambda scripts;

converted;

fixed rulify_prems;

lemmas [mono] = lists_mono;

updated;

fixed make_pp; basic interrupt handling;

improved exit function for polyml-4.0;

tuned

*** empty log message ***

ported HOL/Lambda/ListBeta;

improved handling of messages: do not decorate writeln output;

improved messages;

more polyml choices; tuned;

added some bind_thm

functional LBV style, dead code, type safety -> Isar

MicroJava changed (all of BV -> Isar)

tuned

*** empty log message ***

tuned;

renamed antiquotation 'name' to 'text'; added antiquotation option 'source';

tuned;

added "source" option;

token trans: removed \mbox to achieve proper italic correction;

added string_of;

introduced induct_thm_tac

*** empty log message ***

tuned;

use polyml-version;

*** empty log message ***

*** empty log message ***

fixed name;

New function name_of_typ.

Improved names for size function.

fixed comment;

*** empty log message ***

Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.

added ML-Systems/polyml-4.0.ML;

added \<dots> syntax;

added prems_limit;

added "name" antiq and "indent" option;

pr: added prems limit;

added indent;

\<dots> syntax;

added antiquotation 'name' and option 'indent';

'syntax': improved mode spec; 'pr': prems limit;

improved spacing of Sum, Prod, integral; tuned;

underscore: added \mbox to avoid hyphenation;

* 'pr' command: optional argument for ProofContext.prems_limit;

*** empty log message ***

*** empty log message ***

*** empty log message ***

made SML/XL happy;

updated;

improved isabellepar env;

updated;

Lambda/InductTermi made new-style theory; tuned;

proper cong setup;

Simplifier.cong_add_global;

cong setup now part of Simplifier;

updated cong stuff;

'cong' modifiers;

\isakeywordcharunderscore;

* Isar/Provers: 'simp' method now supports 'cong' modifiers; * Provers: Simplifier.easy_setup; tuned;

tex_index: Latex.tex_trailer;

added tex_trailer;

removed METHOD0; added SIMPLE_METHOD('); added thm_args;

Method.SIMPLE_METHOD';

'induct_tac' / 'case_tac': Method.goal_args';

added 'split' method;

\newenvironment{isabellebody}: version without trivlist;

* \isabellestyle{it} produces near math mode output; * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, XSYMBOL_HOME;

Removed map_compose from simpset.

fixed Id string

updated;

restart_loader: reset_path;

add_path: del_path first;

proper setup of iman.sty/extra.sty/ttbox.sty;

updated;

moved \tt things to ttbox.sty; removed \Pure etc;

proper setup;

removed ttbox;

*** empty log message ***

*** empty log message ***

added \trivlist...\endtrivlist to the "isabelle" environment in order to correct several problems (e.g. need for newlines and %)

moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML

xsymbols for {| and |}

xsymbols for leads-to and Join

fixed strip_assums and assum_pairs, restoring them (essentially) to their 1989 versions. They had been "optimized" for flattened parameters, but failed when given an initial, non-flattened proof state. A manifestation of the bug is Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))"; be exE 1;

added some xsymbols, and tidied

more symbols;

disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);

choosefrom: support easy settings;

choosefrom: easy settings;

isabelle env: trivlist;

removed redundant commands

removed most "makeatother", no longer needed

updated to latest versions of ttbox and ttbreak

updated;

updated;

updated;

tuned translations;