sorting

Added function package to PreList Added sorted/sort to List Moved qsort from ex to Library

change print_mode: CRITICAL;

added print_mode_value (CRITICAL);

avoid direct access to print_mode;

adapted use_text;

platform-sensitive default location for ATP provers

tuned;

HOL/Induct/Common_Patterns.thy

added Induct/Common_Patterns.thy;

moved induct patterns to HOL/Induct/Common_Patterns.thy;

use_file: added ``tune'' argument;

added structure Posix;

with_modes: always CRITICAL;

added ML/ml_parse.ML;

obsolete;

use_text/file: tune text (cf. ML_Parse.fix_ints);

use_text/file: tune text (cf. ML_Parse.fix_ints); activate proper int setup;

added ml_system_fix_ints; use_text/file: tune text (cf. ML_Parse.fix_ints);

added ml_system_fix_ints;

removed obsolete Selector token; tuned signature; string syntax: proper escape format;

tuned message;

Minimal parsing for SML -- fixing integer numerals.

added some int constraints (ML_Parse.fix_ints not active here);

added rudimentary instantiation stub

added explicit theorems

delayed evaluation

clarified class interfaces and internals

introduced classes

multi-functional value keyword

added lemmas for finiteness

tuned

fixed title

replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;

ML_Lex.keywords; tuned comments;

tuned comments;

replaced Symbol.is_hex_letter to Symbol.is_ascii_hex; tuned Symbol.is_ascii_blank (according to SML syntax);

Lexical syntax for SML.

added ML/ml_lex.ML;

removed redundant OuterLex.make_lexicon;

lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy

added "<*mlex*>" which lexicographically combines a measure function with a relation

moved ML_XXX.ML files to Pure/ML;

tidied

reverted back to the old version of the equivariance lemma for ALL

some cleaning up to do with contexts

Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators.

Added equivariance lemmas for induct_forall.

Added equivariance lemma for induct_implies.

typo fixed, dead link removed

added lemma

Auto quickcheck now displays counterexample using Proof.goal_message rather than producing an error message.

added String.isSubstring;

export is_finished; added thy_ord (based on update_time); begin_thy/register_thy: more precise handling of update_time;

Present.session_name;

tuned signature; tuned message;

thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;

removed thy_ord (erratic due to multi-threading);

some cleaning up

theorem: apply hook last;

reset goal messages after goal update;

added hilite markup;

fixed type alias in signature;

added lemma

allow TVars during type inference

tidied the proofs

made smlnj happy;

new fun declaration

Auto-config of E_HOME, SPASS_HOME, VAMPIRE_HOME

Vampire structured proofs. Better parsing; some bug fixes.

chained facts are now included

new proofs found

trivial cleaning up

added goal_message;

theorem hooks: apply in declaration order;

Generalized code generator for numerals.

- New theories Lambda/NormalForm and Lambda/Standardization - Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories

Added lecture notes by Matthes and Loader.

New proof of standardization theorem (inspired by Ralph Matthes).

Definition of normal forms (taken from theory WeakNorm).

Moved definition of normal forms to new NormalForm theory.

Added Standardization theory.

New code generator setup (taken from Library/Executable_Real.thy, also works for old code generator).

Added code generator setup (taken from Library/Executable_Rat.thy, also works for old code generator).

Integrated code generator setup into RealDef theory.

Integrated code generator setup into Rational theory.

Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories.

use preferences.ML: do setmp *here*, to capture intended default values;

tuned;

modified proofs so that they are not using claset()

tuned lemma; replaced !! by arbitrary

Improved comment.

Documented function package in IsarRef-manual.

added variations on infinite descent

fixed Rat.inv

fixed Rat.inv