interface for unchecked definitions

shifted "fun" command to Wellfounded_Relations

updated

Eliminated unused theorems minusinf_ex and minusinf_bex

first working version of instance target

interpretation for typedefs

using intro_locales instead of unfold_locales if appropriate

more canonical attribute application

adjustions to due to instance target

new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.

*** empty log message ***

added {#.,.,...#}

tuned

stripped down

isabelle-process: option -p echos ISABELLE_PID;

commit: non-critical, otherwise session restart will result in deadlock!

instance command as rudimentary class target

dropped dead code

polyml: default heap size is back to -H 200 (people are still using machines with < 1GB of memory; no need to workaround heap problems of polyml-5.0 anymore);

an example file for how to treat Felleisen-Hieb-style contexts in nominal

removed (cf. object_logic.ML);

added base_sort; added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML); typedecl: recovered proper use of Syntax.type_name;

removed typedecl.ML (cf. object_logic.ML);

ObjectLogic.typedecl;

replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);

simplified using sledgehammer

Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.

comment

(reverted to unnamed infix)

simplified interpretations

deleted looping code theorem

to_set now applies collect_mem_simproc as well.

naming policy for instances

tuned interfaces of class module

dropped dead code

dropped legacy unnamed infix

dropped implicit assumption proof

dropped legacy ml bindings

tuned titles;

moved titles;

tuned title;

tuned titles;

standard_parse_term: check ambiguous results without changing the result yet;

challenge by John Harrison: down to 12s (was 17s, was 75s);

Knaster_Tarski: turned into Isar statement, tuned proofs;

first_order_match now only calls loose_bvar when inside an abstraction.

check_conv now only performs beta-eta-normalization when equations cannot be combined just by transitivity.

Optimized beta_norm: only tries to normalize term when it contains abstractions.

Better error messages for cterm_instantiate.

some more lemmas due to Peter Lammich;

Peter Lammich: HOL-Lattice lemmas;

Removed forced roman font in mode=IfThen.

use official polyml-5.1;

tuned comments; tuned;

moved new NEWS from Isabelle2007 to this Isabelle version'';

simplified website rsync

rudimentary instantiation target

explicit type signature

interpretation of typedecls: instantiation to class type

deleted card definition as code lemma; authentic syntax for card

separated typedecl module, providing typedecl command with interpretation

faster metis calls

tuned;

updated to official Poly/ML 5.1;

tuned;

include elapsed time for parallel sessions;

intern_skolem: disallow qualified names;

fixed

dropped diagnostic commands

tuned;

tuned spacing;

updated Proof General advertisement; tuned line breaks;

PolyML.SaveState.loadState: exit on failure;

Init outer syntax after message setup to avoid spurious output.

update to most recent smlnj version

inform_file_processed: made even more robust against bad file specs;

removed unused inform_file_processed; proper_inform_file_processed: check before change (avoids non-linear update); avoid Path.explode here (liberal low-level file names);

init_empty: check before change (avoids non-linear update);

Add thm_dep preference to menu, inadvertently missed off

tuned;

use -source instead of -target;

target 1.4 of JVM;

thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);

isatool version: clarify that this is the *long* form;

ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!

cover ISABELLE_IDENTIFIER;

README for E binary distribution;

tuned;

patching in the latest changes from Hurd

tuned;

some more items;

updated

Added JAR paper by Wenzel and Wiedijk.

Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.

Added TrueE to extraction_expand.

Added new program extraction examples.

New case studies for program extraction.

Moved auxiliary lemmas to separate theory.

Added new exampes Greatest_Common_Divisor and Euclid.

Moved nat_eq_dec to Util.thy

Moved nat_eq_dec and search to Util.thy

Tuned.

to_pred and to_set now save induction and case rule tags.

removed left-over text links from lynx conversion; removed umlauts (cannot assume iso-latin anymore, and not yet utf-8 either);

back to sigusr2, after Poly/ML 5.1 has been adapted;

changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;

updates

updated

reactivated default paragraph formatting for ``proof documents'';

fixed typo;

added signatures; tuned

abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);

simplified Consts.dest; export standard_infer_types;

simplified Consts.dest;

simplified Consts.dest; dest;

updates

avoid ML print in production code;

updated;

auto quickcheck: reduced messages;

notation works with any known constant (including fixes/abbrevs);