isabelle: Changelog

paulson [Tue, 27 May 1997 13:03:41 +0200] rev 3352

New theorems suggested by Florian Kammueller

slotosch [Mon, 26 May 1997 14:54:24 +0200] rev 3351

remoded ccc1

slotosch [Mon, 26 May 1997 13:51:03 +0200] rev 3350

removed ccc1

wenzelm [Mon, 26 May 1997 13:45:39 +0200] rev 3349

tuned comment;

paulson [Mon, 26 May 1997 12:54:40 +0200] rev 3348

Two useful facts about Powersets suggested by Florian Kammueller

paulson [Mon, 26 May 1997 12:53:45 +0200] rev 3347

Added a missing "result();" after problem 43.

paulson [Mon, 26 May 1997 12:44:04 +0200] rev 3346

Tidying using the new exhaust_tac

paulson [Mon, 26 May 1997 12:42:38 +0200] rev 3345

Now recdef checks the name of the function being defined. Slight tidying

paulson [Mon, 26 May 1997 12:40:51 +0200] rev 3344

Deleted option_case_tac because exhaust_tac performs a similar function. Deleted the duplicate proof of expand_option_case...

paulson [Mon, 26 May 1997 12:39:57 +0200] rev 3343

Renamed lessD to Suc_leI

isabelle