nth -> !

nth -> !

feed isabelle session;

commented out symboloutput.pl;

added feeder.pl;

pretty_name_space;

removed declared; improved dest;

removed distinct_fst_string;

improved error handling;

fixed execute;

made MLWorks happy;

stderr to $LOG;

Symtab.empty;

improved internal representation;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;

renamed Symtab.null to Symtab.empty;

added >> : (theory -> theory) -> unit;

tuned;

replaced symtab.ML by table.ML;

renamed (is_)null to (is_)empty; renamed DUPLICATE to DUP; renamed extend_new to extend;

Generic tables (lacking delete operation). Implemented as 2-3 trees.

tuned;

export range_type;

improved comment;

More restrictive patterns to prevent changing comments

New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

Tidied using rev_iffD1

Now Blast_tac works properly

Tidied. Also better proof using new blast_tac

Decremented subscript because of change to iffD1

Tidied using rev_iffD1, etc

Tidied using rev_iffD1

Tidied using more default rules

Overloading info for image

tidied

New rules rev_iffD{1,2}

Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac

New "obvious theorems"

Added range-type for completeness

New example

New rules rev_iffD{1,2}

corrected removal to /tmp/tmp.c

added removal to /tmp/tmp.txt

records without signature

remove signatrue from records

tuned;

new version;

added record.ML;

first version of records

pasted old insertion sort (does not work with new sort function!)

adapted to new sort function;

log file; elapsed time;

leading 0s;

tuned;

adapted to new sort function;

log files; 'clean' target;

tuned;

added rev_order, make_ord; reimplemented sort function: stable version of quicksort;

term order; signature;