a few additions and deletions

tuned;

proper use of PureThy.has_name_hint instead of hard-wired string'';

removed non-modular comment;

new theorem int_infinite

Fix tell_thm_deps to match changse in PureThy.

Expose hard-wired string which was changed and broke Proof General.

clarified error message

clarified command annotation

changed cong alist - now using AList operations instead of overwrite_warn

dropped Output.update_warn

print translation for record types with empty-sorted type variables raise Match instead of producing an error

dropped lemma duplicates in HOL.thy

Tidying; more debugging information. New reference unwanted_types.

Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).

Add get_succs

Add operations on preference tables (remove, set_default).

adjusted to new codegen_funcgr interface

added interface for plugging in preprocessors

additional auxiliary here

whitespace tuning

dropped dead code

shifted import order

dropped whitespace

changed name of interpretation linorder to order

proper simproc_setup; tuned ML setup;

added get_simproc, @{simproc};

added interface for target_naming;

added simproc_setup;

added def_simproc(_i) -- define named simprocs; tuned;

updated;

Now deals with simples cases where the input equations contain type variables See example in ReflectionEx.thy

refined algorithm

clarified code

exported interface for explicit error messages

added NestedEnvironment

Improved debugging

Streamlined and improved debugging messages

more fixes of arithmetic for min/max.

min/max lemmas (actually unused!)

simplification of Suc/numeral combinations with min, max

Fixed long-standing, MAJOR bug in "lt"

adjusted manual to improved treatment of overloaded constants

Allows evaluation of min/max o numerals.

fixed bug for OCaml bigints

tuned

added explicit maintainance of coregular code theorems for overloaded constants

dropped useless stuff

clarified code

added explicit query function for arities to subalgebra projection

not importing NestedEnvironment

adjusted to changes in class package

made executable

improved

fxied bug for OCaml bigints

adjusted names

tuned eta_contract;

updated timing;

some new lemmas

Let <loadfile> execute even while a file is open interactively.

fixes smlnj-related problem, updated signature

added a fold up and fold down as separate functions and fixed zipto to use the folddown.

simplified proofs

Included ex/Fundefs.thy in HOL-ex session

* Preliminary implementation of tail recursion * Clarified internal interfaces

Add location_of_position. Needs work elsewhere.

Test askref

Expose currently open file

Sync location with pgip.rnc, fixing attribute names

Add askrefs, setrefs, error_with_pos

Comments

Comment

Add line_of, name_of destructors.

Added lemma nat_size[simp]: "size (n::nat) = n"

tuned;

improved fact references: thmref; tuned;

added atomic, print_int; tuned;

tuned ML setup;

* ML in Isar: improved error reporting;

tuned;

*** MESSAGE REFERS TO PREVIOUS VERSION *** @{theory}: plain ML_Context.the_context();

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed is_finished_thy;

tuned comments

simplified ML setup;

use_text: added name argument; moved File.use to ML_Context.use; removed the_context_finished;

moved File.use to ML_Context.use;

use_text: added name argument;

Added simproc list_neq (prompted by an application)

Added lists-as-multisets functions

Simple and efficient binary numerals.

added HOL/ex/Binary.thy;

tuned ML setup;

* ML within Isar: antiquotations;

added @{theory};

added the_context_finished; eval_wrapper: Output.debug; simplified antiq signatures; added basic antiquotations; tuned;

Toplevel.debug: coincide with Output.debugging;

ML tactic: proper context for compile and runtime;

tuned;

added @{simpset};

added is_finished_thy;

Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);

tuned ML setup; added @{claset};

added @{clasimpset};

added @{claset};

tuned;

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;