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;