corrected spelling of title (to test new CVS loginfo)

*** empty log message ***

removed incompatibility with sml

removed incompatibility with sml

Documented store_thm and moved qed to top

Added the new Limit.{thy,ML} example

The inverse limit construction -- thanks to Sten Agerholm

corrected spelling of title

All constants introduced by datatype now operate on class term explicitly. They used to take the default class.

Commutation replaces Confluence

corrected some errors that occurred after introduction of local simpsets

corrected title

added newline for last line

added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb

added 8bit pragmas

changed some comments

Confluence became Commutation

Added dependency on Eta

New version with eta reduction.

corrected title

added local simpsets

added local simpsets

corrected $Id$

added local simpsets; removed IOA from 'make test'

removed command for loading Provers/simplifier.ML (now done in Pure/Thy/ROOT)

added removal of theorems if theory is to be reloaded; changed functions for local simpsets

changed usage of structure Simplifier

renamed SS to Simpset; fixed bug in merge_ss

added new example by John Harrison

bicompose_aux: tuned fix_shyps; simplifier: fixed handling of shyps;

added comment;

fixed $Id$

trivial update to POPL title

replaced "IOA/ROOT.ML" by "IOA/ROOT_NTP.ML IOA/ROOT_ABP.ML"

split IOA/ROOT.ML into two files for ABP and NTP

*** empty log message ***

added nested types on right hand side of datatype definitions

removed list2 and enum2

added enum2 and list2

Removed duplicate copy of converse_Un

Various axiomatic type class demos;

the NatClass demo of the axclass tutorial;

fixed bug: duplicate "duplicate" warnings

restored old invocation of use_string till I can make the new version work

added global simpset

added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database

added same_sg and same_thm

adapted to new version of shyps-stuff;

nonempty_sort: no longer var names as args;

considerably tuned shyps handling;

adapted to new version of shyps-stuff;

added check for duplicate theorems in theorem database; changed warnings and error messages in thy_read to distinguish between theorems in theor_y_ database and in theor_em_ database

minor fix to make less noise with SML/NJ;

updated "o" in HOL: (infixl 55) added warning about conj_cong in HOL.

minor corrections to indexing; added thms_containing in header

changed "o" to (infixl 55)

clarified comment

fixed bug in findI removed duplicates in findEs

deactivated fix_shyps.

updated version number to revision 4

Mateja Jamnik's theory to html converter

Handle renaming of CHOL.tex to HOL.tex

minor polishing of text on findI, etc.

Trivial reformatting of reference

corrected bind_thm: now applies "standard" uniformly.

Documented findI, findE, findEs, thms_containing.

Added findI, findEs, and findE.

MAJOR changes: added shyps component to type thm; added rules strip_shyps, implies_intr_shyps; fixed rules to handle shyps properly;

modified prepare_proof to handle shyps;

modified pretty_thm, standard, eq_thm to handle shyps;

modified prep_thm_axm to handle shyps; fixed class_axms: class_trivs *first*; improved axclass_tac: now also handles object rules as witnesses;

added (my own version of) nonempty_sort: sg -> (string * sort) list -> sort -> bool;

added nonempty_sort (a somewhat braindead version!);

Added nonempty_sort.

added section on "Reordering assumptions".

added rotate_tac

changed AC_... to OrdQuant_...

Version of the proof macros for LaTeX 2.09

added rotate_tac.

Ran expandshort and corrected spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Added rev_append and rev_rev_ident to list_ss.

minor fix: instance now raises error if witness axioms don't exist;

Many small changes to make proofs run faster

Now includes all the AC files

tidied proof of add_less_mono

trivial updates to header and bibliography

Numerous small improvements by KG and LCP

match_bvs no longer puts a name in the alist if it is null ("")

Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)

Corrected mixfix declaration of @perm

Proved perm_length

Added two final lines to intro_tacsf for mutual recursion (borrowed from ZF version)

Old version of mutual induction never worked. Now ensures that all predicates get the SAME type. Updated mutual_ind_tac from ZF version

Changed comments

Added Part_Int and Part_Collect for inductive definitions

Includes Sum.thy as a parent for mutual recursion

now uses proof209.sty

trivial update

trivial update

finally deleted

Updated nipkow-prehofer

moved mixfix syntax from sign.ML

moved mixfix syntax to Syntax/mixfix.ML

Added insert_not_empty, UN_empty and UN_insert (to set_ss).

added cargs for curried function application

removed debugging output

remove Old_HOL

added comments; fixed a bug; reduced memory usage slightly

added mention of new theories BT and Perm

new inductive definition: permutations

Renamed some vars.

fixed comment

Proof of n_leaves_reflect uses permutative rewriting.

Added function rev and its properties length_rev, etc.

The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported