summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Mon, 20 Sep 1999 12:01:41 +0200
Fixed bug in add_primrec which caused non-informative error message.

Fixed bug in add_primrec which caused non-informative error message.

renamed Always_Int to Always_Int_I

new theorem mono_Follows_apply

new theorem Always_INT_distrib; therefore renamed Always_Int
to Always_Int_I

working Safety proof for the system at last

now uses Pattern.aeconv, not aconv, to test equality between the terms
abstracted over; otherwise it is incomplete. Other changes are cosmetic

new rule PLam_ensures

working snapshot

new theorem image_image_eq_UN

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);