isabelle: Changelog

paulson [Fri, 27 Nov 1998 10:40:29 +0100] rev 5978

moved diag (diagonal relation) from Univ to Relation

paulson [Thu, 26 Nov 1998 17:40:10 +0100] rev 5977

tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules

mueller [Thu, 26 Nov 1998 16:37:56 +0100] rev 5976

tuning to assimiliate it with PhD;

nipkow [Thu, 26 Nov 1998 12:18:51 +0100] rev 5975

Added a general refutation tactic which works by putting things into nnf first.

nipkow [Thu, 26 Nov 1998 12:18:08 +0100] rev 5974

Added filter_prems_tac

wenzelm [Wed, 25 Nov 1998 20:55:25 +0100] rev 5973

removed prs / prs_fn;

paulson [Wed, 25 Nov 1998 15:55:00 +0100] rev 5972

guarantees laws

paulson [Wed, 25 Nov 1998 15:54:41 +0100] rev 5971

simplified ensures_UNIV

paulson [Wed, 25 Nov 1998 15:53:31 +0100] rev 5970

new thms for invariant

paulson [Wed, 25 Nov 1998 15:53:04 +0100] rev 5969

new theorem program_equalityE

isabelle