updated;

moved ML context stuff to from Context to ML_Context;

renamed IsarOutput to ThyOutput; moved ML context stuff to from Context to ML_Context;

interpreter for Finite_Set.finite added

reformatted to 80 chars/line

Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. This solves the goals like "~ 4 dvd 1". This used to fail before.

adapted ML context operations;

added generic_theory_of; adapted ML context operations;

added 'declaration' command;

added 'declaration' command; adapted ML context operations;

adapted ML context operations;

ML context: full generic context, tuned signature;

updated

Fix pgmlsymbolsoff

tuned a bit the proofs

correctled left/right following of another context in zipto.

induction rules for trancl/rtrancl expressed using subsets

Deleted mk_fol_type, since the constructors can be used directly

Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC minimize_applies is now by default TRUE!

fixed typo introduced by me

changed dictionary representation to explicit classrel witnesses

reverted order of classrels

cleanup

formalisation of Crary's chapter on logical relations (in the book on Advanced Topics in Type Systems) done by Narboux and Urban

added capabilities to handle mutual inductions

refined and added example for ExecutableRat

introduced binding concept

slight cleanup

renamed locale partial_order to order

refined and added example for ExecutableRat

updated keywords

added sections on mutual induction and patterns

optimized translation of HO problems

Reverted to structure representation with records.

more term inspection

introduced binding concept

adjusted manual

well-founded relations for the integers

updated to mention the automatic unfolding of constants

removed NameSpace.split -- use qualifier/base instead;

fixed exit: proper type check of state; tuned signature;

tuned

minor comment change

no unfolding necessary anymore (refute does that automatically now)

improved case patterns

added undefined in cases

named preprocessorts

cleanup

activated new class code

handling for "undefined" in case expressions

named preprocessors

The "of 1, simplified" stopped working some time ago, leaving these simprules open to looking. Now, explicit lemma statements ensure that the correct formula is proved.

More compact proof reconstruction: lines having fewer than !min_deps dependences are folded into the rest of the proof.

simplified the resoution proofs

Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.

Add info fatality for error messages.

Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.

slight cleanups

improved names

proper node names

slight cleanup

improved variable name handling

moved variable environments here

moved a lot to codegen_func.ML

typo

added map_abs_vars

tuned signature;

print functions for typs and terms added

Be more chatty in PGIP file operations.

A few lemmas about relative primes when dividing trough gcd Definition of gcd on integers and a few lemmas.

A few theorems on integer divisibily.

Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever

reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)

added codegen_func.ML

non-layout-sensitive syntax for Haskell

some cleanup

primitive definitions are always eta-expanded

added block_enclose

added CodeEval

dealing with ml_string and char instances

dealing with ml_string combinators

adaptions

removed Toplevel.print_exn hook -- existing error_msg_fn does the job;

RAW-ProofGeneral: more dependencies;

Proof.context now sent to watcher and used in type inference step of proof reconstruction

tuned msg;

removed obsolete ProofGeneral/syntax_standalone.ML;

approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;

added mk_simproc': tuned interface; tuned runtime context: merge with dynamic one;

clarification

dropped function theorems are considered as deleted

examples for evaluation oracle

fixed eval oracle

Be more chatty in PGIP file operations.proof_general_pgip.ML

broken error handling for command syntax -- reverted to revision 1.9;

Use warning fatality

Add warning fatality

improvements to proof reconstruction. Some files loaded in a different order

using Array.modifyi (no functional change)

run as RAW session;

removed obsolete option -C; added option -R: run RAW session;

removed obsolete Pure-copied target; added RAW, RAW-ProofGeneral to test target;

updated manual

updated manual

obsolete sign_of calls removed

fixed output

different handling of eta expansion

eta-expansion now only to common maximum number of arguments

clarified code

more term examples

eliminated Option.app

constants are unfolded, universal quantifiers are stripped, some minor changes

Fix error reporting in Emacs to also match Isar command failure exactly.

Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.

Expose command failure recovery code for top level.

Selected functions from syntax module

x-symbol is no longer switched off in the ATP linkup

Improvements to proof reconstruction. Now "fixes" is inserted

Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction

first version of structured proof reconstruction