the function space operator

New section on advanced datatypes.

*** empty log message ***

mesontest2.ML was never needed in the distribution

changed inverse syntax from x-| to i(x)

proved surjI

tidied

Big simplification of proofs. Deleted lots of unnecessary theorems

tiny changes;

changed to a link;

local simpset theory data; simp add / del attributes; smart_simp_tac and method;

local claset theory data; intro, elim, dest, del attributes; single_tac and method; fast, best etc. methods;

Object logic specific operations.

Isar setups;

added metacuts_tac;

removed local_theory;

exnMessage Interrupt;

added lift_modifier, rule;

added Isar;

added Isar/;

Pure outer syntax.

Non-logical toplevel commands.

Derived theory operations.

The global Isabelle/Isar outer syntax.

The Isabelle/Isar toplevel.

Histories of proof states, with undo / redo and prev / back.

Generic parsers for Isabelle/Isar outer syntax.

Outer lexical syntax for Isabelle/Isar.

Proof methods.

Symbolic theorem attributes.

Concrete argument syntax (for attributes, methods etc.).

Type-safe interface for proof context data.

Proof states and methods.

Proof context information.

Isar -- Intelligible Semi-Automated Reasoning for Isabelle.

Check release name and date in NEWS!

smart interrupt handler;

option -I: startup Isar interaction mode;

isabelle -I;

fake interrupt handler;

simple interrupt_handler;

new Domain/Range rules

new TIMES/Sigma rules

removed obsolete comment and "open" declaration

"Subscribe" link

spell check;

tuned;

added mailing list, removed mirrors;

Revising the Client proof as suggested by Michel Charpentier. New lemmas about composition (in Union.ML), etc. Also changed "length" to "size" because it is displayed as "size" in any event.

made more generic;

Shortened names and added new thm.

Some streamlining of text. Theory library is now assumed to be LOCAL and not at TUM.

tuned;

tuned width of pics;

tuned;

oops;

tuned pics;

made weblint happy;

oops;

Id;

tuned; fixed links;

tuned;

main Isabelle page;

New example

Domain r, Range r replace fst``r, snd``r

increased precedence of unary minus from 80 to 100 requires a similar increase for %# and %%#

increased precedence of unary minus from 80 to 100

Charpentier laws

the Increasing operator

no need for int_0

locales now implicitly quantify over free variables

tuned current_goals_markers;

Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed

Explicit (and improved) simprules for binary arithmetic. New default simprules to eliminate (int 0) and (z + - w)

*** empty log message ***

shyps note for prim. rules;

tuned;

tuned current_goals_markers semantics to avoid empty lines;

tidied

auto update

Some more proofs.

added nat_diff_split and a few lemmas in Trancl.

ML_SYSTEM=polyml-3.1;

tuned checklist;

official release;

ML_SYSTEM factory default;

*** empty log message ***

tuned;

records; tuned datatype, inductive, primrec;

*** empty log message ***

Added theorem bool_induct (for rep_datatype).

Added theorem unit_induct (for rep_datatype).

Added theorems True_not_False and False_not_True (for rep_datatype).

unit and bool are now represented as datatypes.

corrected auto_tac (applications of unsafe wrappers)

corrected (and simplified) depth_tac

corrected auto_tac (applications of unsafe wrappers) by correcting (and simplifying) nodup_depth_tac

corrected auto_tac (applications of unsafe wrappers) improved style of several proofs

added SOLVE tactical

tuned;

matharray; records;

SYNC: records (draft version);

Warns when stack is extended; better decl of print_depth

better checking of "defines" in a locale

better reporting of "Additional hypotheses" in a locale

Now users will never see (int 0)

auto update

updated as requested by Markus

export is_ml_identifier;

Updated to new datatype package.

ex/Points added

Example for records

Directory Induct: Added new theory ABexp, removed obsolete theory Simult.

Added new theory ABexp, removed obsolete theory Simult.

Terms are now defined using the new datatype package.

New example for using the datatype package: Arithmetic and boolean expressions.

Removed obsolete theory Simult (see theory Term).

started to add records;

occurs check now handles Bound variables (for soundness)

updated by isatool logo;