]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a9af753) | patch
New command default "foo" uri1 ... urin
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 14:09:02 +0000 (14:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 14:09:02 +0000 (14:09 +0000)
commitf94eb70000832bc252cd4a510a1ede4d8197a4a8
tree362d77862d8ddd63cbdbbd2370113c80b636fea3tree | snapshot
parenta9af753c66a80cb4f50f32e63272f3830cba306ccommit | diff
New command   default "foo" uri1 ... urin
to set uri1 ... urin as the default foo.

Actually it can be used to set the current equality, true, false and absurd
like this:

default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri.
default "true" trueuri.
default "false" falseuri.
default "absurd" absurduri.
helm/matita/library/equality.ma diff | blob | history
helm/matita/library/logic.ma diff | blob | history
helm/matita/matitaEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.