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.

some optimizations of Larry's

corrected comments

corrected comments

optimized net for matching of abstractions to speed up simplifier

moved misplaced comment

removed Syntax/parse_tree.ML;

optimized the number of eta-contractions in rewriting

added a check for existence of a temporary file before removing it

used unlink for delete_files instead of calling rm

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

ZF/perm/image_comp: new

got rid of METAHYPS due to the change of the basic simplification routines (see update of Pure/{thm,drule,tactic}.ML)

adapted a proof to the new solver (see change of FOL/simpdata.ML)

updated solver of FOL_ss. see change of HOL/simpdata.ML

added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.

added lexical class of type variables

shortened msg

added fake_cterm_of to speed up rewriting

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

changed tracing of simplifier

optimized simplifier - signature of rewritten term stays constant

added "Reading thy-File" message

added subsig: sg * sg -> bool to test if one signature is contained in another.

added sys_error;

fixed a bug in update/next_level which occured when a child wasn't loaded

added empty type-abbr field to extend_theory

added []-field to extend_theory: no type abbreviations.

Added []-field to extend_theory to accomodate type abbreviations.

Necessary changes to accomodate type abbreviations.

pretty_thm is now exported;

new section for equality properties

Updated read_insts to approximate simultaneous type checking of substitution pairs.

added isabelle-users paragraph

added mention of simplifier, splitter, hypsubst

new year

updated instantiate to deal with type clashes

ZF/equalities/SUM_eq_UN: new ZF/equalities: corrected bound variable anomalies in some distributive laws

Pure/tactic/compose_inst_tac: when catching exception THM, prints the message before failing!! This reports the reason for failure in cases like by (res_inst_tac [("P", "?Q(a)")] mp 1); in which ?Q appears in mp with a different type.

deleted harmful basify, which pulled rewrite rules down to base type. Not needed for new simplifier.

added rep_tsig

last minute changes, eg literal tokens -> delimiters and valued tokens -> names.

ZF/univ/in_Vfrom_limit: new ZF/univ/sum_in_Vfrom, etc: streamlined proofs using in_Vfrom_limit

ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new

Typos and style

Changed Acknowledgements

Acknowledged Carsten Clasohm

New distributive laws for Sigma and UN

removal of amssymbols.sty and lcp.sty; addition of iman.sty

ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted them, to make the most of the load-path mechanism. (use_thy adds the new theory to the list of loaded theories.)

minor corrections

new references

now inspects FOLP_build_completed

now declares FOLP_build_completed

*** empty log message ***

*** empty log message ***

ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma, ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN ZF/ex/llist/llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN

changed split_filename, remove_ext; added base_name;

*** empty log message ***

ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many coinduction proofs ZF/quniv: deleted the following obsolete theorems (saved on Isa/old): Int_Vfrom_0_in_quniv Pair_in_quniv_D QInl_Int_Vfrom_succ_in_quniv QInl_Int_quniv_in_quniv QPair_Int_Vfrom_in_quniv QPair_Int_Vfrom_succ_in_quniv QPair_Int_quniv_eq QPair_Int_quniv_in_quniv QPair_Int_quniv_in_quniv product_Int_quniv_eq quniv_Int_Vfrom zero_Int_in_quniv

extend: cleaned up, adapted for new Syntax.extend; extend, merge: improved roots (logical_types) handling;

*** empty log message ***

added (partial) extend_tables; improved extend; fixed roots handling of extend and merge;

changed datatype ext;

improved comments;

added SCANNER; changed scan_any: no longer uses take_prefix;

added Scanner;

added logical_types

improved comments;

added equal, not_equal: ''a -> ''a -> bool

Minor edits to discussion of use_thy

Correction to eta-contraction; thanks to Markus W.

Correction to page 16; thanks to Markus W.

Corrected errors found by Marcus Wenzel.

changed some names and deleted *NORMALIZED*

corrected obvious errors;

corrected obvious errors;

*** empty log message ***

corrected some obvious errors;

changed beginning of "Reading a new theory", added index "automatic loading"

corrected trivial typo;

corrected trivial typo;

fixed a bug in get_filenames, changed output of use_thy

asm_full_simp_tac now fails if there are no subgoals

added subsection 'Classes and types'; added syntax and short explanation of translations section;

added Syntax.read_typ; Syntax.extend: added read_ty, removed def_sort argument;

Sign.extend: Syntax.extend now called with read_ty;

removed section 'Classes and types';

added index commands, removed last paragraph of "Using Poly/ML"

changed itmath trickery to be compatible with NFSS (itmath.sty)

minor changes

added chapter "Defining Theories" and made changes for new Readthy functions

*** empty log message ***

*** empty log message ***

various minor changes;

Fixed bug in rewriter (fun impc) discovered by Marcus Moore.

Reformatting of SIMPLIFIER figure

Trivial spacing corrections

Documents not, and, or, xor: boolean ops

Many edits suggested by Grundy & Thompson

expandshort and other trivial changes

expandshort

Misc modifs such as expandshort

added loaded_thys to signature and removed list_/set_loaded

changed use_thy's parameter to exact theory name

made pseudo theories for all ML files; documented dependencies between all thy and ML files

moved call of store_theory to end of use t.thy; use t.ML; use_thy now needs the exact theory name (capital/lower letters); improved handling of incompletly read theories; added function unlink_thy, removed function relations; added reference variable delete_tmpfile; removed some bugs

replaced \un by \union in "Simplification sets"

changed use_thy's parameter to exact theory name

changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs

boolE: changed to have equality assumptions instead of P(c); proved many boolean laws

Added commentary

fun parents: removed pp block (didn't have any effect)

changed application format for pretty-printer

Misc updates

Misc updates

changed formatting for application

Changed the simplifier: if the subgoaler proves an unexpected thm, chances are, it is an instance of the expected thm. Instead of aborting, rewriting now fails at that point.

Various updates for Isabelle-93

new style file

adapted "Defining theories" to new use_thy

replaced by current version;

replaced by current version;

*** empty log message ***

Initial revision

Initial revision

Initial revision