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

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);

added no_prems;