Isabelle NEWS -- history user-relevant changes

==============================================

New in this Isabelle release

----------------------------

*** General ***

* Provers/simplifier:

  - Completely reimplemented method simp (ML: Asm_full_simp_tac):

    Assumptions are now subject to complete mutual simplification,

    not just from left to right. The simplifier now preserves

    the order of assumptions.

    Potential INCOMPATIBILITY:

    -- simp sometimes diverges where the old version did

       not, e.g. invoking simp on the goal

        [| P (f x); y = x; f x = f y |] ==> Q

       now gives rise to the infinite reduction sequence

        P(f x) --(f x = f y)--> P(f y) --(y = x)--> P(f x) --(f x = f y)--> ...

       Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this

       kind of problem.

    -- Tactics combining classical reasoner and simplification (such as auto)

       are also affected by this change, because many of them rely on

       simp. They may sometimes diverge as well or yield a different numbers

       of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto

       in case of problems. Sometimes subsequent calls to the classical

       reasoner will fail because a preceeding call to the simplifier too

       eagerly simplified the goal, e.g. deleted redundant premises.

  - The simplifier trace now shows the names of the applied rewrite rules

  - You can limit the number of recursive invocations of the simplifier

    during conditional rewriting (where the simplifie tries to solve the

    conditions before applying the rewrite rule):

    ML "simp_depth_limit := n"

    where n is an integer. Thus you can force termination where previously

    the simplifier would diverge.

  - Accepts free variables as head terms in congruence rules.  Useful in Isar.

* Pure: The main goal of the proof state is no longer shown by default, only

the subgoals. This behaviour is controlled by a new flag.

   PG menu: Isabelle/Isar -> Settings -> Show Main Goal

(ML: Proof.show_main_goal).

* Pure: You can find all matching introduction rules for subgoal 1, i.e. all

rules whose conclusion matches subgoal 1:

      PG menu: Isabelle/Isar -> Show me -> matching rules

The rules are ordered by how closely they match the subgoal.

In particular, rules that solve a subgoal outright are displayed first

(or rather last, the way they are printed).

(ML: ProofGeneral.print_intros())

* Pure: New flag trace_unify_fail causes unification to print

diagnostic information (PG: in trace buffer) when it fails. This is

useful for figuring out why single step proofs like rule, erule or

assumption failed.

* Pure: Locale specifications now produce predicate definitions

according to the body of text (covering assumptions modulo local

definitions); predicate "loc_axioms" covers newly introduced text,

while "loc" is cumulative wrt. all included locale expressions; the

latter view is presented only on export into the global theory

context; potential INCOMPATIBILITY, use "(open)" option to fall back

on the old view without predicates;

* Pure: predefined locales "var" and "struct" are useful for sharing

parameters (as in CASL, for example); just specify something like

``var x + var y + struct M'' as import;

* Pure: improved thms_containing: proper indexing of facts instead of

raw theorems; check validity of results wrt. current name space;

include local facts of proof configuration (also covers active

locales), cover fixed variables in index; may use "_" in term

specification; an optional limit for the number of printed facts may

be given (the default is 40);

* Pure: disallow duplicate fact bindings within new-style theory files

(batch-mode only);

* Provers: improved induct method: assumptions introduced by case

"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from

the goal statement); "foo" still refers to all facts collectively;

* Provers: the function blast.overloaded has been removed: all constants

are regarded as potentially overloaded, which improves robustness in exchange

for slight decrease in efficiency;

* Provers/linorder: New generic prover for transitivity reasoning over

linear orders.  Note: this prover is not efficient!

* Isar: preview of problems to finish 'show' now produce an error

rather than just a warning (in interactive mode);

*** HOL ***

* New tactic "trans_tac" and method "trans" instantiate

Provers/linorder.ML for axclasses "order" and "linorder" (predicates

"<=", "<" and "="). 

* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 

HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";

* 'typedef' command has new option "open" to suppress the set

definition;

* functions Min and Max on finite sets have been introduced (theory

Finite_Set);

* attribute [symmetric] now works for relations as well; it turns

(x,y) : R^-1 into (y,x) : R, and vice versa;

* arith(_tac) now produces a counter example if it cannot prove a theorem.

  In ProofGeneral the counter example appears in the trace buffer.

* arith(_tac) does now know about div k and mod k where k is a numeral

of type nat or int. It can solve simple goals like

  "0 < n ==> n div 2 < (n::nat)"

but fails if divisibility plays a role like in

  "n div 2 + (n+1) div 2 = (n::nat)"

* simp's arithmetic capabilities have been enhanced a bit: it now

takes ~= in premises into account (by performing a case split);

* simp reduces "m*(n div m) + n mod m" to n, even if the two summands

are distributed over a sum of terms;

* induct over a !!-quantified statement (say !!x1..xn):

  each "case" automatically performs "fix x1 .. xn" with exactly those names.

* Real/HahnBanach: updated and adapted to locales;

* GroupTheory: converted to Isar theories, using locales with implicit

structures.  Also a new, experimental summation operator for abelian groups;

* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and

Kramer);

* UNITY: added the Meier-Sanders theory of progress sets;

*** ZF ***

* ZF/Constructible: consistency proof for AC (Gödel's constructible

universe, etc.);

* Main ZF: virtually all theories converted to new-style format;

*** ML ***

* Pure: Tactic.prove provides sane interface for internal proofs;

omits the infamous "standard" operation, so this is more appropriate

than prove_goalw_cterm in many situations (e.g. in simprocs);

* Pure: improved error reporting of simprocs;

* Provers: Simplifier.simproc(_i) provides sane interface for setting

up simprocs;

New in Isabelle2002 (March 2002)

--------------------------------

*** Document preparation ***

* greatly simplified document preparation setup, including more

graceful interpretation of isatool usedir -i/-d/-D options, and more

instructive isatool mkdir; users should basically be able to get

started with "isatool mkdir HOL Test && isatool make"; alternatively,

users may run a separate document processing stage manually like this:

"isatool usedir -D output HOL Test && isatool document Test/output";

* theory dependency graph may now be incorporated into documents;

isatool usedir -g true will produce session_graph.eps/.pdf for use

with \includegraphics of LaTeX;

* proper spacing of consecutive markup elements, especially text

blocks after section headings;

* support bold style (for single symbols only), input syntax is like

this: "\<^bold>\<alpha>" or "\<^bold>A";

* \<bullet> is now output as bold \cdot by default, which looks much

better in printed text;

* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;

note that these symbols are currently unavailable in Proof General /

X-Symbol; new symbols \<zero>, \<one>, ..., \<nine>, and \<euro>;

* isatool latex no longer depends on changed TEXINPUTS, instead

isatool document copies the Isabelle style files to the target

location;

*** Isar ***

* Pure/Provers: improved proof by cases and induction;

  - 'case' command admits impromptu naming of parameters (such as

    "case (Suc n)");

  - 'induct' method divinates rule instantiation from the inductive

    claim; no longer requires excessive ?P bindings for proper

    instantiation of cases;

  - 'induct' method properly enumerates all possibilities of set/type

    rules; as a consequence facts may be also passed through *type*

    rules without further ado;

  - 'induct' method now derives symbolic cases from the *rulified*

    rule (before it used to rulify cases stemming from the internal

    atomized version); this means that the context of a non-atomic

    statement becomes is included in the hypothesis, avoiding the

    slightly cumbersome show "PROP ?case" form;

  - 'induct' may now use elim-style induction rules without chaining

    facts, using ``missing'' premises from the goal state; this allows

    rules stemming from inductive sets to be applied in unstructured

    scripts, while still benefitting from proper handling of non-atomic

    statements; NB: major inductive premises need to be put first, all

    the rest of the goal is passed through the induction;

  - 'induct' proper support for mutual induction involving non-atomic

    rule statements (uses the new concept of simultaneous goals, see

    below);

  - append all possible rule selections, but only use the first

    success (no backtracking);

  - removed obsolete "(simplified)" and "(stripped)" options of methods;

  - undeclared rule case names default to numbers 1, 2, 3, ...;

  - added 'print_induct_rules' (covered by help item in recent Proof

    General versions);

  - moved induct/cases attributes to Pure, methods to Provers;

  - generic method setup instantiated for FOL and HOL;

* Pure: support multiple simultaneous goal statements, for example

"have a: A and b: B" (same for 'theorem' etc.); being a pure

meta-level mechanism, this acts as if several individual goals had

been stated separately; in particular common proof methods need to be

repeated in order to cover all claims; note that a single elimination

step is *not* sufficient to establish the two conjunctions, so this

fails:

  assume "A & B" then have A and B ..   (*".." fails*)

better use "obtain" in situations as above; alternative refer to

multi-step methods like 'auto', 'simp_all', 'blast+' etc.;

* Pure: proper integration with ``locales''; unlike the original

version by Florian Kammüller, Isar locales package high-level proof

contexts rather than raw logical ones (e.g. we admit to include

attributes everywhere); operations on locales include merge and

rename; support for implicit arguments (``structures''); simultaneous

type-inference over imports and text; see also HOL/ex/Locales.thy for

some examples;

* Pure: the following commands have been ``localized'', supporting a

target locale specification "(in name)": 'lemma', 'theorem',

'corollary', 'lemmas', 'theorems', 'declare'; the results will be

stored both within the locale and at the theory level (exported and

qualified by the locale name);

* Pure: theory goals may now be specified in ``long'' form, with

ad-hoc contexts consisting of arbitrary locale elements. for example

``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and

definitions may be given, too); the result is a meta-level rule with

the context elements being discharged in the obvious way;

* Pure: new proof command 'using' allows to augment currently used

facts after a goal statement ('using' is syntactically analogous to

'apply', but acts on the goal's facts only); this allows chained facts

to be separated into parts given before and after a claim, as in

``from a and b have C using d and e <proof>'';

* Pure: renamed "antecedent" case to "rule_context";

* Pure: new 'judgment' command records explicit information about the

object-logic embedding (used by several tools internally); no longer

use hard-wired "Trueprop";

* Pure: added 'corollary' command;

* Pure: fixed 'token_translation' command;

* Pure: removed obsolete 'exported' attribute;

* Pure: dummy pattern "_" in is/let is now automatically lifted over

bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")

supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

* Pure: method 'atomize' presents local goal premises as object-level

statements (atomic meta-level propositions); setup controlled via

rewrite rules declarations of 'atomize' attribute; example

application: 'induct' method with proper rule statements in improper

proof *scripts*;

* Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)

now consider the syntactic context of assumptions, giving a better

chance to get type-inference of the arguments right (this is

especially important for locales);

* Pure: "sorry" no longer requires quick_and_dirty in interactive

mode;

* Pure/obtain: the formal conclusion "thesis", being marked as

``internal'', may no longer be reference directly in the text;

potential INCOMPATIBILITY, may need to use "?thesis" in rare

situations;

* Pure: generic 'sym' attribute which declares a rule both as pure

'elim?' and for the 'symmetric' operation;

* Pure: marginal comments ``--'' may now occur just anywhere in the

text; the fixed correlation with particular command syntax has been

discontinued;

* Pure: new method 'rules' is particularly well-suited for proof

search in intuitionistic logic; a bit slower than 'blast' or 'fast',

but often produces more compact proof terms with less detours;

* Pure/Provers/classical: simplified integration with pure rule

attributes and methods; the classical "intro?/elim?/dest?"

declarations coincide with the pure ones; the "rule" method no longer

includes classically swapped intros; "intro" and "elim" methods no

longer pick rules from the context; also got rid of ML declarations

AddXIs/AddXEs/AddXDs; all of this has some potential for

INCOMPATIBILITY;

* Provers/classical: attribute 'swapped' produces classical inversions

of introduction rules;

* Provers/simplifier: 'simplified' attribute may refer to explicit

rules instead of full simplifier context; 'iff' attribute handles

conditional rules;

* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

* HOL: 'recdef' now fails on unfinished automated proofs, use

"(permissive)" option to recover old behavior;

* HOL: 'inductive' no longer features separate (collective) attributes

for 'intros' (was found too confusing);

* HOL: properly declared induction rules less_induct and

wf_induct_rule;

*** HOL ***

* HOL: moved over to sane numeral syntax; the new policy is as

follows:

  - 0 and 1 are polymorphic constants, which are defined on any

  numeric type (nat, int, real etc.);

  - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based

  binary representation internally;

  - type nat has special constructor Suc, and generally prefers Suc 0

  over 1::nat and Suc (Suc 0) over 2::nat;

This change may cause significant problems of INCOMPATIBILITY; here

are some hints on converting existing sources:

  - due to the new "num" token, "-0" and "-1" etc. are now atomic

  entities, so expressions involving "-" (unary or binary minus) need

  to be spaced properly;

  - existing occurrences of "1" may need to be constraint "1::nat" or

  even replaced by Suc 0; similar for old "2";

  - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";

  - remove all special provisions on numerals in proofs;

* HOL: simp rules nat_number expand numerals on nat to Suc/0

representation (depends on bin_arith_simps in the default context);

* HOL: symbolic syntax for x^2 (numeral 2);

* HOL: the class of all HOL types is now called "type" rather than

"term"; INCOMPATIBILITY, need to adapt references to this type class

in axclass/classes, instance/arities, and (usually rare) occurrences

in typings (of consts etc.); internally the class is called

"HOL.type", ML programs should refer to HOLogic.typeS;

* HOL/record package improvements:

  - new derived operations "fields" to build a partial record section,

    "extend" to promote a fixed record to a record scheme, and

    "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*

    declared as simp by default;

  - shared operations ("more", "fields", etc.) now need to be always

    qualified) --- potential INCOMPATIBILITY;

  - removed "make_scheme" operations (use "make" with "extend") --

    INCOMPATIBILITY;

  - removed "more" class (simply use "term") -- INCOMPATIBILITY;

  - provides cases/induct rules for use with corresponding Isar

    methods (for concrete records, record schemes, concrete more

    parts, and schematic more parts -- in that order);

  - internal definitions directly based on a light-weight abstract

    theory of product types over typedef rather than datatype;

* HOL: generic code generator for generating executable ML code from

specifications; specific support for HOL constructs such as inductive

datatypes and sets, as well as recursive functions; can be invoked

via 'generate_code' theory section;

* HOL: canonical cases/induct rules for n-tuples (n = 3..7);

* HOL: consolidated and renamed several theories.  In particular:

	Ord.thy has been absorbed into HOL.thy

	String.thy has been absorbed into List.thy

* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"

(beware of argument permutation!);

* HOL: linorder_less_split superseded by linorder_cases;

* HOL/List: "nodups" renamed to "distinct";

* HOL: added "The" definite description operator; move Hilbert's "Eps"

to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES:

  - Ex_def has changed, now need to use some_eq_ex

* HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so

in this (rare) case use:

  delSWrapper "split_all_tac"

  addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)

* HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS

MAY FAIL;

* HOL: introduced f^n = f o ... o f; warning: due to the limits of

Isabelle's type classes, ^ on functions and relations has too general

a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be

necessary to attach explicit type constraints;

* HOL/Relation: the prefix name of the infix "O" has been changed from

"comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been

renamed accordingly (eg "compI" -> "rel_compI").

* HOL: syntax translations now work properly with numerals and records

expressions;

* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead

of "lam" -- INCOMPATIBILITY;

* HOL: got rid of some global declarations (potential INCOMPATIBILITY

for ML tools): const "()" renamed "Product_Type.Unity", type "unit"

renamed "Product_Type.unit";

* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl

* HOL: removed obsolete theorem "optionE" (use "option.exhaust", or

the "cases" method);

* HOL/GroupTheory: group theory examples including Sylow's theorem (by

Florian Kammüller);

* HOL/IMP: updated and converted to new-style theory format; several

parts turned into readable document, with proper Isar proof texts and

some explanations (by Gerwin Klein);

* HOL-Real: added Complex_Numbers (by Gertrud Bauer);

* HOL-Hyperreal is now a logic image;

*** HOLCF ***

* Isar: consts/constdefs supports mixfix syntax for continuous

operations;

* Isar: domain package adapted to new-style theory format, e.g. see

HOLCF/ex/Dnat.thy;

* theory Lift: proper use of rep_datatype lift instead of ML hacks --

potential INCOMPATIBILITY; now use plain induct_tac instead of former

lift.induct_tac, always use UU instead of Undef;

* HOLCF/IMP: updated and converted to new-style theory;

*** ZF ***

* Isar: proper integration of logic-specific tools and packages,

including theory commands '(co)inductive', '(co)datatype',

'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',

'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

* theory Main no longer includes AC; for the Axiom of Choice, base

your theory on Main_ZFC;

* the integer library now covers quotients and remainders, with many

laws relating division to addition, multiplication, etc.;

* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a

typeless version of the formalism;

* ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory

format;

* ZF/Induct: new directory for examples of inductive definitions,

including theory Multiset for multiset orderings; converted to

new-style theory format;

* ZF: many new theorems about lists, ordinals, etc.;

*** General ***

* Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference

variable proof controls level of detail: 0 = no proofs (only oracle

dependencies), 1 = lemma dependencies, 2 = compact proof terms; see

also ref manual for further ML interfaces;

* Pure/axclass: removed obsolete ML interface

goal_subclass/goal_arity;

* Pure/syntax: new token syntax "num" for plain numerals (without "#"

of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now

separate tokens, so expressions involving minus need to be spaced

properly;

* Pure/syntax: support non-oriented infixes, using keyword "infix"

rather than "infixl" or "infixr";

* Pure/syntax: concrete syntax for dummy type variables admits genuine

sort constraint specifications in type inference; e.g. "x::_::foo"

ensures that the type of "x" is of sort "foo" (but not necessarily a

type variable);

* Pure/syntax: print modes "type_brackets" and "no_type_brackets"

control output of nested => (types); the default behavior is

"type_brackets";

* Pure/syntax: builtin parse translation for "_constify" turns valued

tokens into AST constants;

* Pure/syntax: prefer later declarations of translations and print

translation functions; potential INCOMPATIBILITY: need to reverse

multiple declarations for same syntax element constant;

* Pure/show_hyps reset by default (in accordance to existing Isar

practice);

* Provers/classical: renamed addaltern to addafter, addSaltern to

addSafter;

* Provers/clasimp: ``iff'' declarations now handle conditional rules

as well;

* system: tested support for MacOS X; should be able to get Isabelle +

Proof General to work in a plain Terminal after installing Poly/ML

(e.g. from the Isabelle distribution area) and GNU bash alone

(e.g. from http://www.apple.com); full X11, XEmacs and X-Symbol

support requires further installations, e.g. from

http://fink.sourceforge.net/);

* system: support Poly/ML 4.1.1 (able to manage larger heaps);

* system: reduced base memory usage by Poly/ML (approx. 20 MB instead

of 40 MB), cf. ML_OPTIONS;

* system: Proof General keywords specification is now part of the

Isabelle distribution (see etc/isar-keywords.el);

* system: support for persistent Proof General sessions (refrain from

outdating all loaded theories on startup); user may create writable

logic images like this: ``isabelle -q HOL Test'';

* system: smart selection of Isabelle process versus Isabelle

interface, accommodates case-insensitive file systems (e.g. HFS+); may

run both "isabelle" and "Isabelle" even if file names are badly

damaged (executable inspects the case of the first letter of its own

name); added separate "isabelle-process" and "isabelle-interface";

* system: refrain from any attempt at filtering input streams; no

longer support ``8bit'' encoding of old isabelle font, instead proper

iso-latin characters may now be used; the related isatools

"symbolinput" and "nonascii" have disappeared as well;

* system: removed old "xterm" interface (the print modes "xterm" and

"xterm_color" are still available for direct use in a suitable

terminal);

New in Isabelle99-2 (February 2001)

-----------------------------------

*** Overview of INCOMPATIBILITIES ***

* HOL: please note that theories in the Library and elsewhere often use the

new-style (Isar) format; to refer to their theorems in an ML script you must

bind them to ML identifers by e.g.      val thm_name = thm "thm_name";

* HOL: inductive package no longer splits induction rule aggressively,

but only as far as specified by the introductions given; the old

format may be recovered via ML function complete_split_rule or attribute

'split_rule (complete)';

* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,

gfp_Tarski to gfp_unfold;

* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;

* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a

relation); infix "^^" has been renamed "``"; infix "``" has been

renamed "`"; "univalent" has been renamed "single_valued";

* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"

operation;

* HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;

* Isar: 'obtain' no longer declares "that" fact as simp/intro;

* Isar/HOL: method 'induct' now handles non-atomic goals; as a

consequence, it is no longer monotonic wrt. the local goal context

(which is now passed through the inductive cases);

* Document preparation: renamed standard symbols \<ll> to \<lless> and

\<gg> to \<ggreater>;

*** Document preparation ***

* \isabellestyle{NAME} selects version of Isabelle output (currently

available: are "it" for near math-mode best-style output, "sl" for

slanted text style, and "tt" for plain type-writer; if no

\isabellestyle command is given, output is according to slanted

type-writer);

* support sub/super scripts (for single symbols only), input syntax is

like this: "A\<^sup>*" or "A\<^sup>\<star>";

* some more standard symbols; see Appendix A of the system manual for

the complete list of symbols defined in isabellesym.sty;

* improved isabelle style files; more abstract symbol implementation

(should now use \isamath{...} and \isatext{...} in custom symbol

definitions);

* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals

state; Note that presentation of goal states does not conform to

actual human-readable proof documents.  Please do not include goal

states into document output unless you really know what you are doing!

* proper indentation of antiquoted output with proportional LaTeX

fonts;

* no_document ML operator temporarily disables LaTeX document

generation;

* isatool unsymbolize tunes sources for plain ASCII communication;

*** Isar ***

* Pure: Isar now suffers initial goal statements to contain unbound

schematic variables (this does not conform to actual readable proof

documents, due to unpredictable outcome and non-compositional proof

checking); users who know what they are doing may use schematic goals

for Prolog-style synthesis of proven results;

* Pure: assumption method (an implicit finishing) now handles actual

rules as well;

* Pure: improved 'obtain' --- moved to Pure, insert "that" into

initial goal, declare "that" only as Pure intro (only for single

steps); the "that" rule assumption may now be involved in implicit

finishing, thus ".." becomes a feasible for trivial obtains;

* Pure: default proof step now includes 'intro_classes'; thus trivial

instance proofs may be performed by "..";

* Pure: ?thesis / ?this / "..." now work for pure meta-level

statements as well;

* Pure: more robust selection of calculational rules;

* Pure: the builtin notion of 'finished' goal now includes the ==-refl

rule (as well as the assumption rule);

* Pure: 'thm_deps' command visualizes dependencies of theorems and

lemmas, using the graph browser tool;

* Pure: predict failure of "show" in interactive mode;

* Pure: 'thms_containing' now takes actual terms as arguments;

* HOL: improved method 'induct' --- now handles non-atomic goals

(potential INCOMPATIBILITY); tuned error handling;

* HOL: cases and induct rules now provide explicit hints about the

number of facts to be consumed (0 for "type" and 1 for "set" rules);

any remaining facts are inserted into the goal verbatim;

* HOL: local contexts (aka cases) may now contain term bindings as

well; the 'cases' and 'induct' methods new provide a ?case binding for

the result to be shown in each case;

* HOL: added 'recdef_tc' command;

* isatool convert assists in eliminating legacy ML scripts;

*** HOL ***

* HOL/Library: a collection of generic theories to be used together

with main HOL; the theory loader path already includes this directory

by default; the following existing theories have been moved here:

HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While

(as While_Combinator), HOL/Lex/Prefix (as List_Prefix);

* HOL/Unix: "Some aspects of Unix file-system security", a typical

modelling and verification task performed in Isabelle/HOL +

Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).

* HOL/Algebra: special summation operator SUM no longer exists, it has

been replaced by setsum; infix 'assoc' now has priority 50 (like

'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to

'domain', this makes the theory consistent with mathematical

literature;

* HOL basics: added overloaded operations "inverse" and "divide"

(infix "/"), syntax for generic "abs" operation, generic summation

operator \<Sum>;

* HOL/typedef: simplified package, provide more useful rules (see also

HOL/subset.thy);

* HOL/datatype: induction rule for arbitrarily branching datatypes is

now expressed as a proper nested rule (old-style tactic scripts may

require atomize_strip_tac to cope with non-atomic premises);

* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule

to "split_conv" (old name still available for compatibility);

* HOL: improved concrete syntax for strings (e.g. allows translation

rules with string literals);

* HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals

 and Fleuriot's mechanization of analysis, including the transcendental

 functions for the reals;

* HOL/Real, HOL/Hyperreal: improved arithmetic simplification;

*** CTT ***

* CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that

"lam" is displayed as TWO lambda-symbols

* CTT: theory Main now available, containing everything (that is, Bool

and Arith);

*** General ***

* Pure: the Simplifier has been implemented properly as a derived rule

outside of the actual kernel (at last!); the overall performance

penalty in practical applications is about 50%, while reliability of

the Isabelle inference kernel has been greatly improved;

* print modes "brackets" and "no_brackets" control output of nested =>

(types) and ==> (props); the default behaviour is "brackets";

* Provers: fast_tac (and friends) now handle actual object-logic rules

as assumptions as well;

* system: support Poly/ML 4.0;

* system: isatool install handles KDE version 1 or 2;

New in Isabelle99-1 (October 2000)

----------------------------------

*** Overview of INCOMPATIBILITIES ***

* HOL: simplification of natural numbers is much changed; to partly

recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)

issue the following ML commands:

  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;

  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];

* HOL: simplification no longer dives into case-expressions; this is

controlled by "t.weak_case_cong" for each datatype t;

* HOL: nat_less_induct renamed to less_induct;

* HOL: systematic renaming of the SOME (Eps) rules, may use isatool

fixsome to patch .thy and .ML sources automatically;

  select_equality  -> some_equality

  select_eq_Ex     -> some_eq_ex

  selectI2EX       -> someI2_ex

  selectI2         -> someI2

  selectI          -> someI

  select1_equality -> some1_equality

  Eps_sym_eq       -> some_sym_eq_trivial

  Eps_eq           -> some_eq_trivial

* HOL: exhaust_tac on datatypes superceded by new generic case_tac;

* HOL: removed obsolete theorem binding expand_if (refer to split_if

instead);

* HOL: the recursion equations generated by 'recdef' are now called

f.simps instead of f.rules;

* HOL: qed_spec_mp now also handles bounded ALL as well;

* HOL: 0 is now overloaded, so the type constraint ":: nat" may

sometimes be needed;

* HOL: the constant for "f``x" is now "image" rather than "op ``";

* HOL: the constant for "f-``x" is now "vimage" rather than "op -``";

* HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian

product is now "<*>" instead of "Times"; the lexicographic product is

now "<*lex*>" instead of "**";

* HOL: theory Sexp is now in HOL/Induct examples (it used to be part

of main HOL, but was unused); better use HOL's datatype package;

* HOL: removed "symbols" syntax for constant "override" of theory Map;

the old syntax may be recovered as follows:

  syntax (symbols)

    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"

      (infixl "\\<oplus>" 100)

* HOL/Real: "rabs" replaced by overloaded "abs" function;

* HOL/ML: even fewer consts are declared as global (see theories Ord,

Lfp, Gfp, WF); this only affects ML packages that refer to const names

internally;

* HOL and ZF: syntax for quotienting wrt an equivalence relation

changed from A/r to A//r;

* ZF: new treatment of arithmetic (nat & int) may break some old

proofs;

* Isar: renamed some attributes (RS -> THEN, simplify -> simplified,

rulify -> rule_format, elimify -> elim_format, ...);

* Isar/Provers: intro/elim/dest attributes changed; renamed

intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one

should have to change intro!! to intro? only); replaced "delrule" by

"rule del";

* Isar/HOL: renamed "intrs" to "intros" in inductive definitions;

* Provers: strengthened force_tac by using new first_best_tac;

* LaTeX document preparation: several changes of isabelle.sty (see

lib/texinputs);

*** Document preparation ***

* formal comments (text blocks etc.) in new-style theories may now

contain antiquotations of thm/prop/term/typ/text to be presented

according to latex print mode; concrete syntax is like this:

@{term[show_types] "f(x) = a + x"};

* isatool mkdir provides easy setup of Isabelle session directories,

including proper document sources;

* generated LaTeX sources are now deleted after successful run

(isatool document -c); may retain a copy somewhere else via -D option

of isatool usedir;

* isatool usedir -D now lets isatool latex -o sty update the Isabelle

style files, achieving self-contained LaTeX sources and simplifying

LaTeX debugging;

* old-style theories now produce (crude) LaTeX output as well;

* browser info session directories are now self-contained (may be put

on WWW server seperately); improved graphs of nested sessions; removed

graph for 'all sessions';

* several improvements in isabelle style files; \isabellestyle{it}

produces fake math mode output; \isamarkupheader is now \section by

default; see lib/texinputs/isabelle.sty etc.;

*** Isar ***

* Isar/Pure: local results and corresponding term bindings are now

subject to Hindley-Milner polymorphism (similar to ML); this

accommodates incremental type-inference very nicely;

* Isar/Pure: new derived language element 'obtain' supports

generalized existence reasoning;

* Isar/Pure: new calculational elements 'moreover' and 'ultimately'

support accumulation of results, without applying any rules yet;

useful to collect intermediate results without explicit name

references, and for use with transitivity rules with more than 2

premises;

* Isar/Pure: scalable support for case-analysis type proofs: new

'case' language element refers to local contexts symbolically, as

produced by certain proof methods; internally, case names are attached

to theorems as "tags";

* Isar/Pure: theory command 'hide' removes declarations from

class/type/const name spaces;

* Isar/Pure: theory command 'defs' supports option "(overloaded)" to

indicate potential overloading;

* Isar/Pure: changed syntax of local blocks from {{ }} to { };

* Isar/Pure: syntax of sorts made 'inner', i.e. have to write

"{a,b,c}" instead of {a,b,c};

* Isar/Pure now provides its own version of intro/elim/dest

attributes; useful for building new logics, but beware of confusion

with the version in Provers/classical;

* Isar/Pure: the local context of (non-atomic) goals is provided via

case name 'antecedent';

* Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms

to the current context is now done automatically);

* Isar/Pure: theory command 'method_setup' provides a simple interface

for definining proof methods in ML;

* Isar/Provers: intro/elim/dest attributes changed; renamed

intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in

most cases, one should have to change intro!! to intro? only);

replaced "delrule" by "rule del";

* Isar/Provers: new 'hypsubst' method, plain 'subst' method and

'symmetric' attribute (the latter supercedes [RS sym]);

* Isar/Provers: splitter support (via 'split' attribute and 'simp'

method modifier); 'simp' method: 'only:' modifier removes loopers as

well (including splits);

* Isar/Provers: Simplifier and Classical methods now support all kind

of modifiers used in the past, including 'cong', 'iff', etc.

* Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination

of Simplifier and Classical reasoner);

* Isar/HOL: new proof method 'cases' and improved version of 'induct'

now support named cases; major packages (inductive, datatype, primrec,

recdef) support case names and properly name parameters;

* Isar/HOL: new transitivity rules for substitution in inequalities --

monotonicity conditions are extracted to be proven at end of

calculations;

* Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof

method anyway;

* Isar/HOL: removed old expand_if = split_if; theorems if_splits =

split_if split_if_asm; datatype package provides theorems foo.splits =

foo.split foo.split_asm for each datatype;

* Isar/HOL: tuned inductive package, rename "intrs" to "intros"

(potential INCOMPATIBILITY), emulation of mk_cases feature for proof

scripts: new 'inductive_cases' command and 'ind_cases' method; (Note:

use "(cases (simplified))" method in proper proof texts);

* Isar/HOL: added global 'arith_split' attribute for 'arith' method;

* Isar: names of theorems etc. may be natural numbers as well;

* Isar: 'pr' command: optional arguments for goals_limit and

ProofContext.prems_limit; no longer prints theory contexts, but only

proof states;