tuned;

renamed Isar/isar_output.ML to Thy/thy_output.ML; tuned messages; Antiquote.scan_arguments (moved from here); moved ML context stuff to from Context to ML_Context;

moved ML context stuff to from Context to ML_Context; theorem(s): same kind;

results: proper context;

tuned Scan.extend_lexicon;

renamed IsarOutput to ThyOutput; tuned Scan.extend_lexicon; moved ML context stuff to from Context to ML_Context;

moved parts to spec_parse.ML; tuned signature -- more exports;

removed obsolete Method; added parse (from outer_parse.ML); moved ML context stuff to from Context to ML_Context; tactic: no need to rebind thm/thms;

renamed IsarOutput to ThyOutput; moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

added various ML setup functions (from sign.ML, pure_thy.ML);

removed obsolete Attribute;

tuned signature; added scan_arguments;

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML; load outer_parse.ML early, moved later parts to spec_parse.ML; tuned order;

tuned signature of extend_lexicon;

moved ML translation interfaces to isar_cmd.ML;

moved thm/thms to ml_context.ML; moved generic_setup, add_oracle to isar_cmd.ML;

moved inst from drule.ML to old_goals.ML;

tuned order;

renamed Isar/term_style.ML to Thy/term_style.ML;

renamed Isar/thy_header.ML to Thy/thy_header.ML;

ML context and antiquotations (material from context.ML); added thm/thms (from pure_thy.ML); added support for ML antiquotations;

Parsers for complex specifications (material from outer_parse.ML);

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML;

moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

moved parts of OuterParse to SpecParse;

HOL-Lambda: usedir -m no_brackets;

simplified ML setup;

tuned;

renamed IsarOutput to ThyOutput;

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

Morphism.fact;

Term.lambda: abstract over arbitrary closed terms;

Add standalone file to help porters

Quote arguments in PGIP exceptions. Tune comment.

Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.

Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.

removed dead code;

removed conditional combinator; avoid handle _; showctxt: print_context (cf. local theory context); searchtheorems: proper find_theorems; refrain from setting ml_prompts again; tuned init_pgip;

removed conditional combinator; refrain from setting ml_prompts again; tuned init;

refrain from setting ml_prompts again;

removed misleading OuterLex.eq_token;

pretty_statement: more careful handling of name_hint;

added has_name_hint; name_thm: more careful pre-naming;

removed obsolete name_hint handling;

removed conditional combinator;

removed obsolete support for polyml-4.9.1;

* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;

inform_file_processed: Toplevel.init_empty;

refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned;

Toplevel.init_state;

removed obsolete 'clear_undos';

removed obsolete clear_undos_theory; undo/cannot_undo: proper undo of 'end';

major restructurings

cleanup

improved print of constructors in OCaml

changed syntax for axclass attach

removed obsolete cond_add_path;

removed obsolete context_thy etc.;

removed obsolete init_pgip; removed obsolete redo, context_thy etc.;

removed obsolete init_context;

obsolete (cf. ProofGeneral/proof_general_emacs.ML);

tuned;

signed_string_of_int;

added proper header;

added signed_string_of_int (pruduces proper - instead of SML's ~);

removed obsolete proof_general.ML;

minor tuning;

tuned specifications/proofs;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;

renamed Graph.project to Graph.subgraph;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;

renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;

Sorts.minimal_classes;

classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;

replaced classes by all_classes (topologically sorted); added minimal_classes;

replaced Sign.classes by Sign.all_classes (topologically sorted);

Enable new Proof General code again after SML/NJ compatibility fixes by Florian.

Typo in last commit

explicit construction of operational classes

added handling for explicit classrel witnesses

``classes`` now returns classes in topological order

dropped some bookkeeping

simplified class_package

use_ml: reverted to simple output (Poly/ML changed);

removed private files

tuned;

removed nospaces (Char.isSpace does not conform to Isabelle conventions);

tuned msg;

inlined nospaces (from library.ML);

added

some clarifications

different handling of type variable names

added split

fixed misleading error message

dropped section header

added OCaml code generation (without dictionaries)

removed Haskell reserved words

removed Main.thy

moved code generator product setup here

added code generator test theory

explizit serialization for Haskell id

removed code generation stuff belonging to other theories

moved code generator bool setup here

exported explicit equality on tokens

made SML/NJ happy