Literature references for MiniML.

changed for new naming style of HTML files (leading ".")

added leading "." to HTML filenames

removed quotes from types in consts section

types in consts section of .thy files can now be specified without quotes

removed image borders from index.html files

replaced by index.html

removed green arrow from HTML charts (replaced by "...")

removed borders from images in charts; replaced green arrow by "..."

extended complex_typ

added optional parameters

script for removal of HTML files

renamed chart00 and 00-chart to "index"

renamed logics.html to index.html; added command for cleaning the directory before transfering newer version

renamed logics.html and 00-chart.html to index.html

removed buggy FTP scripts and replaced them by a script for transfer to our HTTP server

scripts for transfer of HTML files to FTP server

removed "duplicate" warning from store_thm_db; changed place where store_thm_db is called for a theory's axioms

added init_html and make_chart

added make_chart

Removed Old_HOL

Unused type sequ deleted

Hat to modify a proof because of chaned simpset for Prod.

Moved some thms to Arith and to Trancl.

Added various thms and tactics.

New theory: type inference for let-free MiniML

added usage of qed

added call of make_chart

added calls of init_html and make_chart; added usage of qed to LK.ML

added calls of init_html and make_chart

entry page for HTML version of Isabelle's logics

added calls of init_html and make_chart; added usage of qed

added calls of init_html and make_chart

added images for HTML files

added generation of HTML files to thy_read.ML; removed old HTML package

added space_explode and relative_path

added "execute"

Improved a few proofs.

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