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;

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

corrected polymorphism check

clarified code for building function equation system; explicit check of type discipline

moved evaluation to Code_Generator.thy

added filter_set; adaptions to more strict type discipline for code lemmas

moved transitivity rules to Orderings.thy

added transitivity rules, reworking of min/max lemmas

dropped dependency on sets

reworking of min/max lemmas

added interpretation

removed HOL_css

added evaluation oracle

replaced exists_fresh lemma with a version formulated with obtains; old lemma is available as exists_fresh' (still needed in apply-scripts)

updated;

Auxiliary antiquotations for Isabelle manuals.

common antiquote_setup.ML;

Arity clauses are now produced only for types and type classes actually used.

converted to 'inductive2';

added for_simple_fixes, specification;

replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);

removed fix_frees interface; added auto_fixes (depends on body mode);

converted to 'inductive2'; proper localized definitions; added rec examples;

inductive: canonical specification syntax (flattened result only); inductive_cases: local_theory; mk_cases/ind_cases: removed legacy code, proper treatment of fixed variables; get_inductive etc.: Proof.context; removed old trace/debug code; tuned;

inductive2: canonical specification syntax; ind_cases2: proper treatment of fixed variables;

InductivePackage.add_inductive_i: canonical argument order;

inductive2: canonical specification syntax;

Exported some names

simplified Proof.theorem(_i) interface -- removed target support; removed obsolete global_goal interface; removed goal_names, simplified goal kind output; tuned;

simplified Proof.theorem(_i) interface; simplified goal kind output;

antiquotation theory: plain Theory.requires, no peeking at ThyInfo;

simplified Proof.theorem(_i) interface;

tuned antiquotation theory;

value restriction

removed old cygwin wrappers;

declare_constraints: reset constraint on dummyS;

removed Isar/isar_thy.ML;

added dummyS;

removed legacy read/cert/string_of; removed obsolete IsarThy.theorem_i; tuned comments;

recdef_tc(_i): local_theory interface via Specification.theorem_i; incorporated IsarThy into IsarCmd;

incorporated IsarThy into IsarCmd;

removed theorem(_i); incorporated into IsarCmd;

upd

atbroy51 broke down, switch to atbroy9

updated

antiquotation "theory": proper output, only check via ThyInfo.theory;

tuned;

added antiquotation @{theory name};

fixed comment -- oops;

adjusted to new fun''

*** empty log message ***

added antiquotation theory

cleaned up

added theory antiquotation

combinator for overwriting changes with warning

added higher-order combinators for structured results

adjusted name in generated code

dropped LOrder dependency

moved upwars in HOL theory graph

added thy dependencies

PreList = Main - List

introduces preorders

dropped Inductive dependency

dropped Typedef dependency

added LOrder dependency

tuned ml antiquotations

adjusted

tuned

added tt tag

auto_term => lexicographic_order

updated

replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup.

added fresh_prodD, which is included fresh_prodD into mksimps setup;

added lexicographic_order.ML to makefile

image_constant_conv no longer [simp]

instantiate: tuned indentity case;

removed dead code;

mk_atomize: careful matching against rules admits overloading;

started reorgnization of lattice theories

Added in is_fol_thms.

level: do not account for local theory blocks (relevant for document preparation);

local 'end': no default tags; tag parser: do not swallow trailing newlines;

* Local theory targets ``context/locale/class ... begin'' followed by ``end''.

removed obsolete context;

turned 'context' into plain thy_decl, discontinued thy_switch;

tuned proofs;

updated local theory targets; removed 'context' as theory switch;

updated local theory targets; added 'context' as local theory switch; tuned;

updated;

Update standard keyword files.

tuned comments; back to fast String.compare (almost no difference in performance);

tuned comments;

tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments;

removed obsolete ML compatibility fragments;

avoid strange typing problem in MosML;

tuned names of start_timing,/end_timing/check_timer;

simplified local theory wrappers;

removed mapping; added reinit;

simplified exit; added reinit;

simplified LocalTheory.exit;

Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented

deleted all uses of sign_of as it's now the identity function

tuned;

tuned Variable.trade;

introduces canonical AList functions for loop_tacs

minor refinements

redundancy checkes includes eta-expansion

improved syntax

added bounded_linear and bounded_bilinear locales

no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);

tuned comments;

added x86-cygwin;

oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.

LocalTheory.restore;

init: '-' refers to global context; provide reinit operation;

abbrevs: return result; LocalTheory.restore;

Stack.map_top;

abbrevs: return result; separate reinit/restore;

separate map_top/all;

abbrevs: return result (use LocalTheory.abbrevs directly);

tuned;

abbrevs: return result;

timing/tracing code removed

interpreters for fst and snd added

new CCS-based implementation that should work with PolyML 5.0

HOL: less/less_eq on bool, modified syntax;

removed obsolete locale_results;

tuned;

imports Binimial;

updated;

lfp_induct_set;

modified less/less_eq syntax to avoid "x < y < z" etc.;

added lemma mult_mono'

added LIM_norm and related lemmas

moved theories Parity, GCD, Binomial to Library;

added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)

incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;

case_tr': proper handling of authentic consts;

removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);

renamed DatatypeHooks.invoke to all

moved lemma eq_neq_eq_imp_neq to HOL

renamed Lattice_Locales to Lattices

abstract ordering theories

obsolete (cf. ROOT.ML);

added structure Main (from Main.ML);

proper definition of add_zero_left/right;

removed NatArith.thy, Main.ML;

removed theory NatArith (now part of Nat);

* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".

moved contribution note to CONTRIBUTORS;

Made "termination by lexicographic_order" the default for "fun" definitions.

LIM_compose -> isCont_LIM_compose; cleaned up and reorganized sections

generalized types of of_nat and of_int to work with non-commutative types

untabified

complex goal statements: misc cleanup;

Added datatype hook to declare all case_congs as "fundef_cong" automatically.

removed obsolete theorem statements (cf. specification.ML);

tuned specifications;

fixed locale fact references;

removed obsolete print_state_hook;

theorem statements: incorporate Obtain.statement, tuned;

moved statement to specification.ML;

removed obsolete Locale.smart_theorem;

avoid handling of arbitrary exceptions;

field-update in records is generalised to take a function on the field rather than the new value.

exported intro_locales_tac ----------------------------------------------------------------------

Proper theorem names at last, no fakes!! Added set_prover function to set various parameters to improve success rate. Fixed the auto settings for E.

some corrections

adjusted title

simplified dest_eq; do not export debuging stuff; has_tvars: actually check all types within a term, not just its resulting type; tuned;

commented out parts which have been inactive (unintentionally) for a long time;

removed obsolete dest_eq_typ;

tuned hypsubst setup;

continued

made locale partial_order compatible with axclass order; changed import order; consecutive changes

made locale partial_order compatible with axclass order

adjusted two lemma names due to name change in interpretation

changed import order

Added a (stub of a) function tutorial

Preparations for making "lexicographic_order" part of "fun"

renamed 'const_syntax' to 'notation';

'const_syntax' command: allow fixed variables, renamed to 'notation';

replaced const_syntax by notation, which operates on terms; read_const: include type;

Isar.context: proper error;

replaced const_syntax by notation, which operates on terms;

read_const: include type;

renamed 'const_syntax' to 'notation'; proper notation for fixed variables;

updated;

Adapted to changes in FixedPoint theory.

method exported

updated NEWS

* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.

added gfx

dropped blastdata.ML

(adjustions)

two further lemmas on split

removed dependency of ord on eq

removed itrev as inlining theorem

added state monad to HOL library

code generator module naming improved

(continued)

(continued)

minor cleanup

case_tr: do not intern already internal consts;

updated;

removed isactrlconst;

instantiate: avoid global references;

added const_syntax_name;

removed obsolete first_duplicate;

added syntax_name;

fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;

Sign.const_syntax_name;

added gfx

removed checkpoint interface; moved back to copy/checkpoint instead of checkpoint/checkpoint (NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate; NB 2: copying a checkpoint always produces a related theory); present_proof: proper treatment of history; tuned;

String.compare: slow version -- performance test;

replaced apply_copy by apply'; tuned;

removed is_Trueprop (use can dest_Trueprop'' instead);

removed is_Trueprop (use can dest_Trueprop'' instead); tuned list_all;

updated;

HOL_USEDIR_OPTIONS: -p 1 by default;

tuned;

* October 2006: Stefan Hohe, TUM;

replaced Toplevel.proof_to_theory by Toplevel.end_proof;

optional argument for timespan (default 100);

added at-mac-poly-e, at64-poly-e;

moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs

new Deriv.thy contains stuff from Lim.thy

re-added simpdata.ML

new ML serializer

fixed problem with eta-expansion

tuned

fixed problem with variable names

tightened notion of function equations

dropped name_mangler.ML

some example tweaking

added particular test for partially applied case constants

improved evaluation setup

adapted to changes in codegen_data.ML

added code gen II

simplified reasoning tools setup

dropped prop_cs

dropped equals_conv for nbe

first version of style guide

continued tutorial

added serialization keywords

bugfix to zipto: left and right were wrong way around.

added sum_squared

changed a misplaced "also" to a "moreover" (caused a loop somehow)

changed to not compile Iteration and Recursion, but Lam_Funs instead

move DERIV_sumr from Series.thy to Lim.thy

generalize type of lemma isCont_Id

new proof of Bseq_NSbseq using transfer

changed to use Lam_Funs

clauses for iff-introduction, unfortunately useless

tuned

Numerous cosmetic changes. Use of ---> notation for types. Added rules for the introduction of the iff connective, but they are too prolific to be useful.

not needed anymore

these files are superseded by the internal recursion combinator and the file Lam_Funs.thy

More blacklisting CASC mode now always on, due to switch to Vampire 8.1 (i.e. the 2006 version) Now runs ATPs unless time_limit = 0.

added lexicographic_order tactic

new SML serializer

clarified make_term interface

introduced CodegenData.add_func_legacy

cleaned up

adapted seralizer syntax

adapted to new serializer syntax

constructing proof

dropped constructiv `->

new serialization syntax; experimental extensions

refined

refined algorithm

simplified preprocessor framework

cleanup

*** empty log message ***

fixed type signature of Type.varify

dropped junk

disabled some code generation (an intermeidate solution)

adapted to new serializer syntax

added Equals_conv

cleaned up

adaptions to changes in preprocessor

dropped nth_update

Purely cosmetic

new file for defining functions in the lambda-calculus

Added "recdef_wf" and "simp" attribute to "wf_measures"

Removed debugging output

removed free "x" from termination goal...

Added "measures" combinator for lexicographic combinations of multiple measures.

Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted

adapted to Stefan's new inductive package

Fixed bug in the handling of congruence rules

(added entry)

switched merge_alists'' to AList.merge'' whenever appropriate

new single-step proofs

meson method MUST NOT use all safe rules, only basic ones for the logical connectives.

Improved tracing

fixed two bugs

bugfixes

added example with split

cleanup in ML setup code

added option of Haskell serializer

continued

Added freshness context to FCBs.

Adapted to changes in FCBs.

Added Compile and Height examples.

Added Compile and Height examples to Nominal directory.

removed antisym_setup.ML

cleaned up

final Haskell serializer

dropped classop shallow namespace

added Haskell

added reserved words for Haskell

slight cleanup

extended section on code generator

small refinements

continued

added entries for tutorials

Proof of "bs # fK bs us vs" no longer depends on FCBs.

example of a single-step proof reconstruction

Fixed the "exception Empty" bug in elim2Fol Also added a check to suppress elimination rules that would yield too many clauses More debugging info

Added more debugging info

nclauses no longer requires its input to be in NNF

cleanup

explicit change of code width possible

code nofunc now permits theorems violating typing discipline

abandoned foldl

fold cleanup

slight cleanup

slight adaption

added normal post setup; cleaned up "execution" constants

added normal post setup

added if_delayed

started tutorial

code_constsubst -> code_axioms

Symtab.foldl replaced by Symtab.fold

Induction rule for graph of recursion combinator is now hidden to prevent name collisions with induction rule for nominal datatype.

Split up FCBs into separate formulae for each binder.

cleaning up

adapted to Stefan's new inductive package and cleaning up

Switched function package to use the new package for inductive predicates.

More robust error handling in make_nnf and forward_res

Stylistic improvements.

Restructured and repaired code dealing with case names in induction and elimination rules.

macbroy6 still has non-standard setup

moved HOL code generator setup to Code_Generator

slight cleanup

fixed print translations for bounded quantification

added explicit print translation for nat_case

added isactrlconst

Order and lattice structures no longer based on records.

add experimental macbroy6 (intel-darwin)

add experimental at64 poly-4.9.1 test on atbroy101

generate devel snapshot even if experimental builds fail. experimental builds are those whose log files fit the pattern isatest-*e.log

added peek;

added theorem(_i);

export map_elem; added read_context_statement_i (internal locale name);

added assert;

theorem: added local_theory version;

Attrib.pretty_attrib;

added pretty_attribs (from attrib.ML);

moved pretty_attribs to attrib.ML;

locale begin/end;

updated;

Added keywords for new inductive definition package.

Adapted to changes in FixedPoint theory.

Moved old inductive package to old_inductive_package.ML

Completely rewrote inductive definition package. Now allows to define n-ary predicates directly (rather than sets of n-tuples), using generalized fixpoint theory for arbitrary complete lattices.

Old version of inductive definition package (for sets).

Moved old inductive package to old_inductive_package.ML

Adapted to new inductive definition package.

Adapted to changes in FixedPoint theory.

Legacy ML bindings now refer to old inductive definition package.

Added new package for inductive definitions, moved old package to old_inductive_package.ML

Generalized gfp and lfp to arbitrary complete lattices.

Repaired strip_assums_hyp (now also works for goals not in hhf normal form).

improved framework

refined

fixed bug

tuned

added codegen2 example

added the missing freshness-lemmas for nat, int, char and string and also the lemma for permutation acting on if's

lifted claset setup from ML to Isar level

explicit nonfix for union and inter

renamed enter_forward_proof to enter_proof_body; renamed exit_local_theory to end_local_theory; added local_theory_to_proof; tuned;