isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

new proof of drop_prog_correct for new definition of project_act
1999-09-21, by paulson
project_act no longer has a special case to allow identity actions
1999-09-21, by paulson
fixed SOUNDNESS BUG concerning the map from terms like ?f x y to SVC variables
1999-09-21, by paulson
Fixed bug in add_primrec which caused non-informative error message.
1999-09-20, by berghofe
renamed Always_Int to Always_Int_I
1999-09-20, by paulson
new theorem mono_Follows_apply
1999-09-20, by paulson
new theorem Always_INT_distrib; therefore renamed Always_Int
1999-09-20, by paulson
working Safety proof for the system at last
1999-09-20, by paulson
now uses Pattern.aeconv, not aconv, to test equality between the terms
1999-09-20, by paulson
new rule PLam_ensures
1999-09-17, by paulson
working snapshot
1999-09-10, by paulson
new theorem image_image_eq_UN
1999-09-10, by paulson
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
1999-09-10, by wenzelm
added no_prems;
1999-09-09, by wenzelm
minor change to smp_tac
1999-09-09, by oheimb
fixed url;
1999-09-09, by wenzelm
AddXDs [bspec];
1999-09-09, by wenzelm
tuned;
1999-09-09, by wenzelm
AddXIs [disjI1, disjI2];
1999-09-09, by wenzelm
removed obsolete comment;
1999-09-09, by wenzelm
lemma less_add;
1999-09-08, by wenzelm
(un)fold: ignore facts;
1999-09-08, by wenzelm
more rational theorem names (?)
1999-09-08, by paulson
tidied
1999-09-08, by paulson
more rational theorem names (?)
1999-09-08, by paulson
ensures_tac now handles leadsTo as well as LeadsTo
1999-09-08, by paulson
new theorem single_Diff_lessThan
1999-09-08, by paulson
now uses the identity function
1999-09-08, by paulson

less more | (0) -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle