]> matita.cs.unibo.it Git - helm.git/commit
new shortcuts
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 31 May 2005 13:01:29 +0000 (13:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 31 May 2005 13:01:29 +0000 (13:01 +0000)
commit0a9583936e33eb9d65361537fd1e05168d423d11
treef106410e2eb81e64aaea444be0039d0d0542c9d9
parent8afcedb6b71f75aac2662629e7f9171085f5e1c2
new shortcuts
fixed hint uri chooser
helm/matita/matita.glade
helm/matita/matita.ml
helm/matita/matitaGui.ml
helm/matita/matitaGui.mli
helm/matita/matitaScript.ml