Comment: see RFC 2396 for relative URI syntax.

Send full paths in PGIP version of file loaded/retracted messages

Conversion of "equal" to "=" for TSTP format; big tidy-up

Lemma "fundef_default_value" uses predicate instead of set.

The function package declares the [code] attribute automatically again.

exported mk_base_funs for use by size-change tools

ATP linkup now generates "new TPTP" rather than "old TPTP"

more careful declaration of "inducts";

tuned;

prefer Proof.context over Context.generic;

prefer Proof.context over Context.generic; tuned;

tuned proofs;

Accept URLs of form file:/home... also.

prefer antiquotations over LaTeX macros;

updated;

renamed Args.Name to Args.Text;

uniform interface for type_syntax/term_syntax/declaration, dependent on morphism; tuned some morphisms;

uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;

Morphism.thm_morphism;

renamed Name value to Text, which is *not* a name in terms of morphisms;

removed obsolete alphanum;

str_of_char: improved output of non-printables;

added head_name_of;

added name/var/typ/term/thm_morphism; removed transfer;

declarations: pass morphism (dummy);

added ISABELLE_IDENTIFIER; removed THIS_IS_ISABELLE_BUILD magic;

ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;

fixed some typos

tuned the proof of the strong induction principle

typo in comment fixed

Add retractfile to supported pgip commands

PGIP: add retractfile. Be stricter in file open/close protocol.

replaced Args.map_values/Element.map_ctxt_values by general morphism application;

moved ML identifiers to structure ML_Syntax;

added morph_ctxt, morph_witness; removed ctxt/witness in favour of general morphisms;

replaced map_values by morph_values;

moved string_of_pair/list/option to structure ML_Syntax;

moved ML syntax operations to structure ML_Syntax;

Basic ML syntax operations.

Abstract morphisms on formal entities.

added morphism.ML, General/ml_syntax.ML;

renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;

removed dead code;

Add doccomment; rename litcomment -> doccomment

* settings: ML_IDENTIFIER includes the Isabelle version identifier;

Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties

ML_IDENTIFIER includes Isabelle version;

add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;

consts: ProofContext.set_stmt true -- avoids naming of local thms;

init: enter inner statement mode, which prevents local notes from being named internally;

more careful declaration of "intros" as Pure.intro;

Fix to local file URI syntax. Add first part of lexicalstructure command support.

completed class parameter handling in axclass.ML

added Isar syntax for adding parameters to axclasses

forced name prefix for class operations

example tuned

no explicit check for theory Nat

added code lemmas

does not import Hilber_Choice any longer

cleanup

incorporated structure HOList into HOLogic

dropped eq const

removed Extraction dependency

final draft

made SML/NJ happy;

theorem(_i): note assms of statement;

removed obsolete simple_note_thms;

added assmsN;

* Isar: the assumptions of a long theorem statement are available as assms;

activated x86_64-linux;

renamed Proof.put_thms_internal to Proof.put_thms;

simplified Proof.theorem(_i); moved theorem kinds from PureThy to Thm;

added stmt mode, which affects naming/indexing of local facts; renamed put_thms_internal to put_thms; notes: proper name and kind (outside of proof body); removed dead code;

simplified theorem(_i); notes: proper kind; renamed put_thms_internal to put_thms;

notes: proper kind; simplified Proof.theorem(_i); context_statement: ProofContext.set_stmt after import;

notes: proper kind;

removed kind attribs;

moved theorem kinds from PureThy to Thm; exported note_thms(s);

moved theorem kinds from PureThy to Thm;

LocalTheory.notes/defs: proper kind;

LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i);

simplified Proof.theorem(_i);

LocalTheory.axioms/notes/defs: proper kind; context_notes: ProofContext.set_stmt after import;

Optimized class_pairs for the common case of no subclasses

Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists

New transformation of eliminatino rules: we simply replace the final conclusion variable by False

run poly-4.9.1 as stable and poly-4.2.0 as experimental on at

removed legacy ML setup;

converted legacy ML scripts;

converted legacy ML scripts;

HOL-Prolog: converted legacy ML scripts;

start at-sml earlier and on different machine, remove sun-sml test (takes too long)

HOL-Algebra: converted legacy ML scripts;

profiling disabled

code thms for classops violating type discipline ignored

cleanup

added instance for class size

added combinators and lemmas

using class instance

dvd_def now with object equality

op div/op mod now named without leading op

workaround for definition violating type discipline

moved dvd stuff to theory Divides

re-eliminated thm trichotomy

power is now a class

tuned

clarified module dependencies

div is now a class

reduced verbosity

adjustments for class package

added an intro lemma for freshness of products; set up the simplifier so that it can deal with the compact and long notation for freshness constraints (FIXME: it should also be able to deal with the special case of freshness of atoms)

more robust syntax for definition/abbreviation/notation;

'notation': more robust 'and' list;

updated;

added Isar.goal;

added where_;

add lemmas LIM_zero_iff, LIM_norm_zero_iff

Includes type:sort constraints in its code to collect predicates in axiom clauses.

Now includes only types used to instantiate overloaded constants in arity clauses

added General/basics.ML;