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

revised for new make_clauses

tidying the ATP communications

string primtives

deactivated test for the moment

fixed typo in comment

Experimenting with interpretations of "definition".

clarified code

dropped superfluos code

code clarifications

import path made absolute

added code lemmas for quantification over bounded nats

Disable new Proof General code until SML/NJ compile fixed.

Use new Proof General code by default [see comment for reverting]

change from "Array" to "Vector"

add lemmas Standard_starfun(2)_iff

Missing elements from doc_markup_elements

Remove obsolete prefixes from error and warning messages.

added isatool codegen

dropped CodegenPackage.const_of_idf

improvements in syntax handling

added Thyname.* and * constant expressions

introduces "__" naming policy

switched argument order in *.syntax lifters

added gen_reflection_tac

now testing executable content of nearly all HOL

dropped debug cmd

explicit nonfix declaration for ML "subset"

dropped two inline directives

introduced abstract view on number expressions in hologic.ML

whitespace fix

added code generation syntax for some char combinators

infix syntax for generated code for composition

new-style oracle setup

added functions tutorial

Add abstraction for objtypes and documents.

removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy

moved several theorems; rearranged theory dependencies

hypreal_of_hypnat abbreviates more general of_hypnat

tracing instead of warning

updated;

removed obsolete assert;

renamed LocalTheory.assert to affirm;

tuned -- accomodate Alice;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

remove Hyperreal/fuf.ML

remove commented section

remove ultra tactic and redundant FreeUltrafilterNat lemmas

declare insert_iff [simp]

activated improved use_ml, which captures output and reports source positions; define use_file in terms of use_ml;

tuned;

prove hyperpow_realpow using transfer

remove usage of ultra tactic

add lemmas singleton and insert_iff

generalized type of hyperpow; removed hcpow

redefine hSuc as *f* Suc, and move to HyperNat.thy

proper use of IntInf instead of InfInf;

defs/notes: more robust transitivity reasoning;

added trans_terms/props;

locale: print context for begin;

remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq

remove uses of star_n and FreeUltrafilterNat

remove use of FreeUltrafilterNat

added lemmas about hRe, hIm, HComplex; removed all uses of star_n

fixed type

added stub for OCaml serializer

cleanup

whitespace correction

clarifed comment

dropped FIXME comment

clarified character setup

remove references to star_n

SComplex abbreviates Standard

simplified mk/dest_numeral (cf. mk/dest_binum of 1.65); put signature into canonical order;

removed legacy ML bindings;

updated;

tuned signature;

internal_abbrev: observe print mode;

target_abbrev: internal mode for abbrevs; tuned;

edge: actually apply operation!

tuned;

authentic syntax for number_of

introduced mk/dest_numeral/number for mk/dest_binum etc.

fixed syntax for bounded quantification

dropped superfluous header

clarified error message

nat type now has a size functin => no longer needed as special case

simplified

local_abbrev: proper fix/declare of local entities;

Deleted the unused type argument of UVar

tuned comments;

added IsarAdvanced/Functions

generalized some lemmas; removed redundant lemmas; cleaned up some proofs

remove uses of scaleR infix syntax; add lemma Reals_number_of

tuned;

add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);

updated;

simplified unlocalize_mixfix;

removed is_class -- handled internally; begin: is_class argument; added fork_mixfix; abbrev/defs: internal_abbrev produces hypothetical term;

notation: Term.equiv_types; add_abbrev: tuned signature, added assumption export; added local_abbrev; tuned;

abbrev: tuned signature;

tuned expand_term;

classified show/thus as prf_asm_goal, which is usually hilited in PG;

tuned expand_binds;

tuned error messages;

added equiv_types;

add_abbrev: tuned signature;

added expand_term_frees;

abbreviate: tuned signature;

LocalTheory.abbrev;

removed redundant constants and lemmas

additions to HOL-Complex

Removal of the "keep_types" flag: we always keep types!

make SML/NJ happy;

made SML/NJ happy;

consistent naming for FreeUltrafilterNat lemmas; cleaned up

cleaned up; generalized some proofs

fix assumptions on NSDERIV_quotient

changed (ns)deriv to take functions of type 'a::real_normed_field => 'a

generalize some theorems

add type annotation

read_xnum: return leading_zeros, radix;

authentic syntax for Pls/Min/Bit; separated translation functions from HOLogic functionality;

authentic syntax for Pls/Min/Bit;

binary numerals: restricted to actual abstract syntax; tuned;

Hyperreal/FrechetDeriv.thy

theory of Frechet derivatives

specials: include single quote;

xstr: disallow backslashes;

advanced translation functions: Proof.context; abs/binder_tr: disallow internal names for bounds;

advanced translation functions: Proof.context;

added improved versions of use_text/file (still inactive);

added use_file;

load secure.ML after symbol.ML, when default output is active;

ordered lists instead of tables for resolving hyps; speedup

nominal_primrec now prints initial proof state.

Abbreviations can now be specified simultaneously with introduction rules.

Adapted to new inductive definition package.

added ProofGeneral settings;

tuned comments;

tuned;

defs: increased entropy of mixfix handling;

fixed term_of_list;

Concrete syntax for hex chars and strings.

renamed str_of_XXX to print_XXX;

HOLogic cleanup;

ML_Syntax.print_XXX;

misc cleanup -- removed non-HOL operations; nibble/char/list/string: observe conventions for abstract syntax operations;

moved char/string syntax to Tools/string_syntax.ML; HOLogic cleanup;

added Tools/string_syntax.ML; tuned;

removed junk;

interpretation: use C_class name prefix;

abs/binder_tr': support printing of idtdummy;

respects2: tuned spacing;

support printing of idtdummy;

added is_class (approximation); added abbrev; tuned;

LocalTheory.notation/abbrev;

extract_case: Name.clean;

added target_notation/abbrev; tuned;

added notation/abbrev (from term_syntax.ML);

tuned absdummy;

added no_frees; add_abbrev: tuned handling of frees, temp workaround;

removed (cf. proof_context.ML and local_theory.ML);

removed Isar/term_syntax.ML;

avoid internal name O_;

hide const linorder.less_eq_less.max linorder.less_eq_less.min;

hardwired option -q;

added print_abbrevs; tuned;

renaming

Modified lattice locale

updated;

added internal_mode;

simplified abbrev: single argument;

TermSyntax.abbrev; ProofContext.set_expand_abbrevs;

added read/pretty_term_abbrev, print_abbrevs; tuned Consts signature; renamed expand_abbrevs to set_expand_abbrevs;

init_context: reset naming;

added 'print_abbrevs';

added print_abbrevs; exit: less verbosity;

added term_abbrev;

renamed reserved to reserved_names; added reserved: Name.context;

tuned Consts signature;

abbrevs: print original rhs;

abbreviate: always authentic, force expansion of internal abbreviations; tuned signature; tuned;

ML_Syntax.reserved(_names);

TermSyntax.abbrev;

added antiquotation abbrev;

added print_abbrevs;

tuned use_text; eval command line: skip over -q option;

added 'help' command (same of 'print_commands');

more careful evaluation of ML text, prevents spurious output;

date: forcing LC_ALL=C prevents funny file names;

root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);

patched up the proofs agsin

removed use of put_name_hint, as the ATP linkup no longer needs this

reorganized structure Tactic vs. MetaSimplifier;

begin/end blocks; tuned notation;

abbrevs: more careful interpretation, avoid dynamic references to local names;

definition/abbreviation: single argument;

simplified add_abbrev -- single argument;

removed obsolete references to ProofGeneral/isa;

added input_mode;

tuned print_locale output; add_decls: Thm.internalK;

moved notation/abbrevs to TermSyntax;

expand_term: based on Envir.expand_term; tuned;

thms etc.: proper treatment of internal_fact with selection;

tuned pretty_src output;

simplified add_abbrevs: no mixfix;

added expand_term;

tuned;

Common term syntax declarations.

added Isar/term_syntax.ML;

TermSyntax.notation/abbrevs;

Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.

Removal of theorem tagging, which the ATP linkup no longer requires,

Poly/ML 5.0 setup for Isabelle2005.

reorganized structure Goal vs. Tactic;

export: added explicit term operation;

abbrevs: actually observe target_morphism;

added expand; export: added explicit term operation;

moved hidden_polymorphism to term.ML;

added hidden_polymorphism (from variable.ML);

add_abbrevs: moved common parts to consts.ML;

abbreviate: improved error handling, return result;

export: added explicit term operation; tuned export_morphism -- lean closure;

LocalDefs.expand;

Improved tracing

no timing;

simplified ML bindings;

simplified ML bindings -- moved to HOL.thy; removed confusing simpset_basic/simplify;

added basic ML bindings;

added aliases for nat_recs/cases;

removed legacy ML bindings; simplified ML setup; tuned declarations;

reduced to genuine legacy bindings -- others in HOL.thy;

removed legacy ML bindings;

target_name: allow qualified names;

add_notation: permissive about undeclared consts; add_abbrevs: allow qualified names; tuned;

generic_goal: enable stmt mode;

encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;

notation/abbreviation: more serious handling of morphisms;

print_syntax etc.: plain Toplevel.context_of;

attribute value: morphism;

add_notation: permissive about undeclared consts;

added mapping_result;

added ML-Systems/polyml-5.0.ML;

Attrib.internal: morphism;

removed duplicate abbreviations (implicit inheritance);

restored notation for less/less_eq (observe proper order of mixfix annotations!); simplified notation for greater/greater_eq, which is only used for input; removed duplicate abbreviations (implicit inheritance);

Document structure in pgip_markup.ML. Minor fixes.

Type alias for XML content

setup for polyml-5.0;

set DYLD_LIBRARY_PATH as well;

Fix typo. Some cleanup for XML attributes

Add dependency for new Emacs PG code

Support PGIP communication for preferences in Emacs mode.

more careful indexing of local facts;

* Pure: official theorem names and additional comments are now strictly separate.

thm/prf: separate official name vs. additional tags;

thm/prf: separate official name vs. additional tags; write_to_file: Path.T;

notes: added non-official name;

note_thmss: added kind tag and non-official name;

Add separate PG Emacs configuration

Include pgip markup module

Build instructions for new Proof General module [not yet activated]

Forward compatibility with new Proof General module.

New files.

Revamped Proof General interface.

Add parse_string for attribute values and other string content

added Ramsey.thy to Library imports, to include it in the daily builds

fixed definition syntax

theory Alloc no longer works -- quick_and_dirty;

converted legacy ML script;

Minor.

Add output function

Add string buffer getter. Add Rawtext constructor to allow XML-escaped strings in tree.

Type abbreviations for element args and attributes

meta_term_syntax: proper operation on untyped preterms;

generalized type signature of foldSet, fold

added some support for embedded terms;

TLA: converted legacy ML scripts;

non-exported syntax

made SML/NJ happy

slight cleanup in hologic.ML

some syntax cleanup

stripped some legacy bindings

Added missing "standard"

Deleted dead code

Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs

notes: proper naming of thm proof, activated import_export_proof;

added full_name;

notes: more careful treatment of Goal.close_result; tuned;

note_thmss: refrain from closing the derivation here;

notes: proper import/export of proofs (still inactive); Goal.norm/close_result; tuned;

removed obsolete (export_)standard;

added mixfix';

added merge_list;

zero_var_indexes_inst: multiple terms; tuned;

Theory.merge_list;

qualified MetaSimplifier.norm_hhf(_protect);

added norm/close_result (supercede local_standard etc.);

added zero_var_indexes_list; removed local_standard (cf. Goal.norm/close_result); instantiate: more precise handling of indexes;

Goal.norm/close_result;

simplified syntax for 'definition', 'abbreviation';

*** bad commit -- reverted to previous version ***

removed export_standard_morphism; Assumption.assms_of: cterm;

simplified add_thmss; mark predicate definitions as internal;

added map/burrow_facts; exported name_multi, name_thm;

added INCR_COMP, COMP_INCR;

tuned;

reworked notes: towards proper import/export of proof terms; tuned;

removed export_standard_morphism;

renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD';

added export; removed find_def, expand_defs;

tuned spaces/comments;

simplified method setup; reactivated dead code;

simplified method setup;

simplified method setup; tuned oracle setup;

clauses sorted according to term order (significant speedup in some cases)

Assumption.assms_of: cterm; added tmp version of export_standard_facts;

Element.generalize_facts;

removed export_standard_morphism; Assumption.assms_of: cterm;

simplified add_thmss; mark predicate definitions as internal;

added facts_map; replaced export(_standard)_facts by generalize_facts; tuned;

added map/burrow_facts; exported name_multi, name_thm;

COMP_INCR;

added INCR_COMP, COMP_INCR;

assms_of: cterm;

simplified Logic.count_prems;

tuned proofs;

go back to fixed atbroy51, fix at-poly-e path settings

Removed the references for counting combinators. Instead they are counted in actual clauses.

added strict_subset

added add_fixed;

simplified '?' operator; defs: more robust transitivity proofs, expand target defs as well; tuned;

simplified '?' operator; note_thmss: no naming;

simplified '?' operator; added expand_defs;

added burrow_fact; no export of name_thms(s);

dest_term: strip_imp_concl;

simplified '?' operator;

Added in another function clause_name_of.

Goals in clause form are sent to the relevance filter.

Call the right inform_file_processed function on <closefile>

Tidied code. Bool constructor is not needed.

tidied code

outermost universal quantifiers are stripped

typo fixed

added the function for free variables of a lambda-term, which is a tad more difficult to define than capture-avoiding substitution

outermost universal quantifiers are stripped

adapted function definitions to new syntax

Adapted to new nominal_primrec command.

additional bookkeeping for class target

small syntax tuning

introduced Simpdata structure

added Trueprop_conv

restructured some proofs

tuned keyword setup for SML code generator

moved order arities for fun and bool to Fun/Orderings

removed HOL structure

adjusted syntax for internal code generation

Added nominal_primrec command.

Adapted to new nominal_primrec command.

Added nominal_primrec.ML

Implemented new "nominal_primrec" command for defining functions on nominal datatypes.

Additional information about nominal datatypes (descriptor, recursion equations etc.) is now stored in theory.

converted legacy ML scripts;

Remove add_master_files which stripped paths for retracted files. Emacs PG already supports full paths here.

* Pure: syntax constant for foo (binder) is called foo_binder;

extend_trtab: allow identical trfuns to be overwritten;

tuned;

Binder: syntax const is determined by binder_name, not its syntax;

simplified consts: no auxiliary params, sane mixfix syntax; declarations: proper morphisms; added target_morphism/name;

abbrevs: no result; Element.map_ctxt_attrib;

added export_(standard_)morphism;

Element.map_ctxt_attrib;

abbrevs: no result; added target_morphism/name; simplified theory prefix (no option); proper morphing of abbrevs/notation;

added map_ctxt_attrib;

abbrevs: no result;

added morh_result, the_inductive, add_inductive_global; removed get_inductive; more careful treatment of result naming/morphing;

InductivePackage.add_inductive_global;

updated (binder) syntax/notation;

tuned morphisms;

added export_morphism; ProofContext.init;

simultaneous fact morphism;

added type_map;

added cterm_rule;

fake predeclaration of structure ProofContext;

added export_morphism;

ProofContext.init;

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