isabelle: Changelog

renamed int-prover.ML to intprover.ML, used exact theory names for use_thy

renamed int-prover.ML to intprover.ML, used exact theory names in ROOT.ML

now forbids semicolons in the body of br, etc. No longer requires it to end the line.

Minor changes; addition of counit.ML

change of my address

Added documenation of change_simp.

renamed co_inductive.ML to coinductive.ML

renamed twos-compl.ML to twos_compl.ML

renamed some files

commented out install_pp for term, typ

added infix delsimps

added function del_simps

deletion of obsolete/private files; update of README

minor changes e.g. datatype_elims

now uses datatype_intrs and datatype_elims

updated version to October 93

no longer specifies "-h 15000". Instead $ISABELLECOMP should include any switch settings.

corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files)

added white-space; made ~: a fake infix;

added white-space; made ~= a fake infix;

removed a bug that occured when a path was specified for use_thy's parameter and the theory was created in a .ML file

ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere

renamed some files

added -h 15000 for Poly/ML in Makefile, changed ROOT.ML for new Readthy

changes in Readthy: - reads needed base theories automatically - keeps a time stamp for all read files - update function - checks for cycles - path list that is searched for files - reads theories that are created in .ML files - etc.

delete_file now has type string -> unit in both NJ and POLY, use of Pure/Thy/ROOT has been moved to the end of Pure/ROOT again

changes for new Readthy

sample datatype defs now use datatype_intrs, datatype_elims

ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works ZF/intr-elim/elim_rls: applied make_elim to succ_inject! ZF/fin: changed type_intrs in inductive def ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks, data_elims ZF/list: now uses datatype_intrs

tactic/fold_tac,fold_goals_tac: now handle critical pairs on the right sides of the defs

goals/print_top,prepare_proof: now call \!print_goals_ref

Pure/drule/print_goals_ref: new, for Centaur interface Pure/tctical/tracify,print_tac: now call !print_goals_ref Pure/goals/print_top,prepare_proof: now call !print_goals_ref

/NJ,POLY/delete_file: new

simpdata/basify: now calls new fastype_of

logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of. So it no longer checks t properly -- but it never checked u anyway, and all existing calls are derived from certified terms...

now calls new fastype_of in three places

Pure/Syntax/printer/is_prop: now calls fastype_of1

Pure/term/fastype_of1: renamed from fastype_of Pure/term/fastype_of: new, takes only one argument (like type_of) Pure/Syntax/printer/is_prop: now calls fastype_of1 Pure/pattern: now calls new fastype_of in three places Pure/logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of. So it no longer checks t properly -- but it never checked u anyway, and all existing calls are derived from certified terms...

renamed: S4.thy to s4.thy, S43.thy to s43.thy, T.thy to t.thy

renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*

file_info now returns a string that does not contain the path/filename (so the string doesn't change when the relative path does)

added parser.ML, install_pp.ML

ZF/ex/tf/tree,forest_unfold: streamlined the proofs Updated other inductive def examples as per changes in the package.

ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE

classical/swap_res_tac: recoded to allow backtracking

Added gen_all to simpdata.ML.

renamed ordinal.thy to ord.thy

renamed ordinal.ML to ord.ML

renamed ordinal.* to ord.*

"The" now a binder, removed translation; improved encoding and translations of tuples; added parse rules for -> and *, removed ndependent_tr;

removed ndependent_tr (no longer needed, use _K);

*** empty log message ***

fixed comment;

added parse rule for "<*>"; removed ndependent_tr;

@List: replaced "args" by "is";

*** empty log message ***

added cons, rcons, last_elem, sort_strings, take_suffix; improved tack_on;

added raise_type: string -> typ list -> term list -> 'a; added raise_term: string -> term list -> 'a;

"The error/exception above ...": errorneous goal now quoted;

used ~: for "not in"

added ~: for "not in"

examples now use ~= for "not equals"

ifol.thy: added ~= for "not equals"

changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split)

rename list-fn to listfn

changed "list-fn" to "listfn"

tctical/dummy_quant_rl: specifies type prop to avoid the type variable ?'a from occurring -- which sometimes caused SELECT_GOAL to fail

Retrying yet again after network problems

Modification of examples for the new operators, < and le.

Retry of the previous commit (network outage)

ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI

added functions that operate on filenames: split_filename (originally located in Pure/read.ML), tack_on, remove_ext

replaced id by idt; added parse rules for --> and *; removed ndependent_tr;

added parse rules for -> and *; removed ndependent_tr;

replaced id by idt; added parse rule for ->; removed ndependent_tr;

Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..';

Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs;

lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;

asm_full_simp_tac now fails when applied to a state w/o subgoals.

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed called expandshort

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10

Added ex_ex1I: new introduction rule for the EX! quantifier.

Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a rule's premises against a list of other proofs.

This commit should not have been necessary. For some reason, the previous commit did not update genrec.ML. There were still occurrences of SIMP_TAC. Was the commit perhaps interrupted??

make-all now has set +e so that New Jersey runs will continue even if some logic fails. change_simp added to help change to new simplifier.

Installation of new simplfier. Previously appeared to set up the old simplifier to rewrite with the partial ordering [=, something not possible with the new simplifier. But such rewriting appears not to have actually been used, and there were few complications. In terms.ML setloop was used to avoid infinite rewriting with the letrec rule. Congruence rules were deleted, and an occasional SIMP_TAC had to become asm_simp_tac.

Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is particularly delicate. There is a variable renaming problem in ramsey.ML/pigeon2_lemma. In some cases, rewriting by typechecking rules had to be replaced by setsolver type_auto_tac... because only the solver can instantiate variables.

Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.

test commit

added header

defined local addcongs

moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm

changed addcongs to addeqcongs in simplifier.ML

Initial revision