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;

moved some fundamental concepts to General/basics.ML;

Fundamental concepts.

add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);

tuned proofs;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules;

dropping accidental self-imports