post-CRC corrections

changed translation of type applications according to new grammar;

added many more filenames to FILES and EX_FILES

made a few cosmetic changes

final Springer copy

final Springer copy

renamed theory files

fixed a small bug

changed convention for theory file names: they now have to consist of the exact theory name + extension

renamed theory files

renamed theory files

renamed theory files

renamed theory files

renamed theory files

renamed theory files

final Springer copy

final Springer copy

final Springer copy

changed the way a grammar is generated to allow the new parser to work; also made a lot of changes in parser.ML and minor ones elsewhere

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

penultimate Springer draft

restored the signature constraint :THM

modifications towards final draft

modifications towards final draft

changed lists and added "let" and "case"

Changed term ordering for permutative rewrites to be AC-compatible.

revisions to first Springer draft

added section on type synonyms

minor problems

added \iflabelundefined

removed inconsistency with new HOL version

Franz fragen

structural induction for strict lists

Franz fragen

revisions to first Springer draft

have broken line

final CADE version

first draft of Springer volume

first draft of Springer volume

first draft of Springer volume

changed "." to "$" and added parentheses to eliminate ambiguity

changed "." to "$" to eliminate ambiguity

Implemented "ordered rewriting": rules which merely permute variables, such as commutativity, are only applied if the term becaomes lexicographically smaller (according to some fixed ordering on the term structure).

first draft of Springer book

first draft of Springer book

first draft of Springer book

First draft of Springer book

new type declaration syntax instead of numbers

FOL/simpdata: tidied FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q"

CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD h:X.Y to fix the variable name h:X.

CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T CCL/ccl.ML/CCL_ss: now includes po_refl RS P_iff_T

Improved layout for inductive defs

adapted type definition to new syntax

fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;

changed "x" to "uu" for implicit name of the dependent type variable

update towards LNCS

deleted a comment

*** empty log message ***

improved explode_tr;

minor update because HOL-lemma changed

tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new

moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML

double_complement_Un: new

*** empty log message ***

improved eq_sg; cosmetical change in print_sg;

added eq_set;

correction to cut tactics

no longer removes *.z

now makes HOLCF

added strs, big_list, writeln;

added simple_string_of_typ, simple_pprint_typ; various internal changes;

added type 'syntax'; added syntax_consts (_K, _explode, _implode, ...);

minor internal changes;

syntax for type abbreviations;

(this is a preliminary release) type abbreviations;

added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";

replaced pprint_sg by Sign.pprint_sg; added Syntax.simple_pprint_typ;

replaced eq_sg by Sign.eq_sg;

removed eq_sg, pprint_sg, print_sg (now in sign.ML); removed cterm_fun, read_ctyp (now in thm.ML); print_theory: now shows all contents;

major cleanup; added eq_sig; added print_sg (full contents), pprint_sg (stamps only); added certify_typ, certify_term; changed read_typ: result now certified;

extend_theory: changed type of "abbrs" arg; added cterm_fun, read_ctyp (from drule.ML); ctyp_of, cterm_of, etc.: now use Sign.certify_...; assumption: now uses Envir.is_empty; bicompose_aux: fixed BUG (unifier with empty "asol" but non-empty "iTs" wasn't applied); fixed axioms_of;

made error message "file not found" more informative

case was renamed to sum_case

added is_empty: env -> bool, minidx: env -> int option;

added HOLCF

removed square and fact

HOLCF examples

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.

commented out sig constraint of functor (for debugging purposes);

changed SYNTAX_FILES;

contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;

minor internal changes;

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension; added translations for _explode, _implode (experimental);

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension;

added some utils: commas, breaks, fbreaks, block, parents, list, str_list;

cosmetic changes;

minor cleanup; added extend, merge; added {lookup,make,dest}_multi;

major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;

corrected comment

Updated refs to old Sign functions

Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g

Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.