new "respects" syntax for the congruent operator

*** empty log message ***

float2real is now globally available

Matrix theory

Matrix theory, linear programming

new theorem symD

listrel operator for lifting relations to lists

Fix file:/// and file://localhost/ to give absolute paths

Fix file:/// and file://localhost/ to return local file result

Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.

new example of a quotiented nested data type

added code to make use of case splitting to prove the specification equations for recursive definitions.

fixed presentation

new "respects" syntax for quotienting

new functions for sets of lists

reference to cla.ML replaced by Classical.thy

commentar eliminated a line 156 - arith raised Match exception at m dvd 2

corrected

m dvd t where m is non numeral is now catched!

Provers/blast.ML: depth_limit

depth limit (previously hard-coded with a value of 20) made a reference

comment modified

changes

begin_theory now takes optional path (current directory) as argument. This is needed for locating *.ML files connected with theories.

Fixed several bugs related to path specifications in theory names.

Function check_file now takes optional path (current directory) as an argument.

Adapted to new interface of function ThyLoad.check_file

Added function for "normalizing" absolute paths (i.e. dereferencing of symbolic links; the functions in path.ML cannot do this). This is used by function full_path.

new isatool dimacs2hol

initial version