]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoprogress.
Andrea Asperti [Fri, 8 Feb 2008 17:04:43 +0000 (17:04 +0000)]
progress.

16 years agoA formalization of modified realisability with truth as in
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 15:22:32 +0000 (15:22 +0000)]
A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.

16 years agoBug fixed in generation of elimination principles of inductive types having
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 13:44:54 +0000 (13:44 +0000)]
Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.

16 years agoprodT merged with prod
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 11:50:42 +0000 (11:50 +0000)]
prodT merged with prod
fstT merged with fst
sndT merged with fst

16 years agoProdT was a perfect copy of Prod. Removed.
Claudio Sacerdoti Coen [Thu, 7 Feb 2008 18:08:50 +0000 (18:08 +0000)]
ProdT was a perfect copy of Prod. Removed.
Sum is now in Type.

16 years agoResults about Chebyshev teta function.
Andrea Asperti [Thu, 7 Feb 2008 12:02:01 +0000 (12:02 +0000)]
Results about Chebyshev teta function.

16 years agocic defined (half)
Enrico Tassi [Tue, 5 Feb 2008 17:45:38 +0000 (17:45 +0000)]
cic defined (half)

16 years agoSome more theorems.
Andrea Asperti [Tue, 5 Feb 2008 16:21:37 +0000 (16:21 +0000)]
Some more theorems.

16 years agoreindent
Enrico Tassi [Tue, 5 Feb 2008 16:12:33 +0000 (16:12 +0000)]
reindent

16 years agooldenv2newenv cache
Enrico Tassi [Tue, 5 Feb 2008 16:06:20 +0000 (16:06 +0000)]
oldenv2newenv cache

16 years agouri and references(uri)
Enrico Tassi [Tue, 5 Feb 2008 15:54:52 +0000 (15:54 +0000)]
uri and references(uri)

16 years agouri -> reference (2)
Enrico Tassi [Tue, 5 Feb 2008 15:23:08 +0000 (15:23 +0000)]
uri -> reference (2)

16 years agouri -> reference
Enrico Tassi [Tue, 5 Feb 2008 15:20:38 +0000 (15:20 +0000)]
uri -> reference

16 years agolower bound for neper's constant
Wilmer Ricciotti [Tue, 5 Feb 2008 15:10:20 +0000 (15:10 +0000)]
lower bound for neper's constant

16 years agosad snapshot
Enrico Tassi [Mon, 4 Feb 2008 15:13:59 +0000 (15:13 +0000)]
sad snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 11:00:54 +0000 (11:00 +0000)]
snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 10:57:45 +0000 (10:57 +0000)]
snapshot

16 years agoImproved approximations for A and prim.
Andrea Asperti [Mon, 4 Feb 2008 08:55:10 +0000 (08:55 +0000)]
Improved approximations for A and prim.

16 years agoSome improvement.
Andrea Asperti [Mon, 4 Feb 2008 08:39:17 +0000 (08:39 +0000)]
Some improvement.

16 years agovery bad bug found, asert false in cicReduction when a clear is performed
Enrico Tassi [Fri, 1 Feb 2008 09:29:09 +0000 (09:29 +0000)]
very bad bug found, asert false in cicReduction when a clear is performed

16 years agoOne Obj.magic implemented, trust changed to false.
Wilmer Ricciotti [Thu, 31 Jan 2008 16:30:40 +0000 (16:30 +0000)]
One Obj.magic implemented, trust changed to false.

16 years agoTransformation back and forth between old and new representation
Wilmer Ricciotti [Thu, 31 Jan 2008 16:20:46 +0000 (16:20 +0000)]
Transformation back and forth between old and new representation

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 15:27:47 +0000 (15:27 +0000)]
snapshot

16 years agonew uri defined
Enrico Tassi [Thu, 31 Jan 2008 15:06:31 +0000 (15:06 +0000)]
new uri defined

16 years agoSquare root added.
Wilmer Ricciotti [Thu, 31 Jan 2008 14:51:45 +0000 (14:51 +0000)]
Square root added.

16 years agosnapshot]
Enrico Tassi [Thu, 31 Jan 2008 14:50:19 +0000 (14:50 +0000)]
snapshot]

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 12:43:37 +0000 (12:43 +0000)]
snapshot

16 years agoadded meta for the new kernel
Enrico Tassi [Wed, 30 Jan 2008 16:29:04 +0000 (16:29 +0000)]
added meta for the new kernel

16 years agostub functions to make all compile
Enrico Tassi [Wed, 30 Jan 2008 16:26:06 +0000 (16:26 +0000)]
stub functions to make all compile

16 years agobasic organization of the new kernel
Enrico Tassi [Wed, 30 Jan 2008 10:42:22 +0000 (10:42 +0000)]
basic organization of the new kernel

16 years agoImproved approximations
Andrea Asperti [Wed, 30 Jan 2008 09:13:06 +0000 (09:13 +0000)]
Improved approximations

16 years agoNew approximtions.
Andrea Asperti [Tue, 29 Jan 2008 10:57:02 +0000 (10:57 +0000)]
New approximtions.

16 years ago...
Enrico Tassi [Thu, 24 Jan 2008 10:37:11 +0000 (10:37 +0000)]
...

16 years agosnapshot with more duality, almost where we left without duality
Enrico Tassi [Wed, 23 Jan 2008 12:44:39 +0000 (12:44 +0000)]
snapshot with more duality, almost where we left without duality

16 years ago...
Enrico Tassi [Tue, 22 Jan 2008 17:54:05 +0000 (17:54 +0000)]
...

16 years agoBertrand's conjecture (weak), some work in progress
Wilmer Ricciotti [Tue, 22 Jan 2008 10:41:43 +0000 (10:41 +0000)]
Bertrand's conjecture (weak), some work in progress

16 years agosnapshot
Enrico Tassi [Mon, 21 Jan 2008 18:05:11 +0000 (18:05 +0000)]
snapshot

16 years agoMatitac now accepts multiple targets :-) (but only in the same root :-(
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:35:11 +0000 (17:35 +0000)]
Matitac now accepts multiple targets :-) (but only in the same root :-(

16 years agoHack for code extraction re-linked, but disactivated.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:30:35 +0000 (17:30 +0000)]
Hack for code extraction re-linked, but disactivated.

16 years agoOld tiny freescale experiment get rid of.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:29:48 +0000 (17:29 +0000)]
Old tiny freescale experiment get rid of.
New shiny freescale formalization by Cosimo Oliboni <oliboni@cs.unibo.it>,
described in his Laurea Thesis.

16 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:18:32 +0000 (17:18 +0000)]
Typo fixed.

16 years agosnopshot before isabellization
Enrico Tassi [Mon, 21 Jan 2008 11:21:36 +0000 (11:21 +0000)]
snopshot before isabellization

16 years agosnapshot
Enrico Tassi [Wed, 16 Jan 2008 15:48:53 +0000 (15:48 +0000)]
snapshot

16 years ago3.27 ok
Enrico Tassi [Wed, 16 Jan 2008 13:32:05 +0000 (13:32 +0000)]
3.27 ok

16 years agoyes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!
Enrico Tassi [Wed, 16 Jan 2008 12:04:06 +0000 (12:04 +0000)]
yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

16 years agoupdate: upper bound for prim
Wilmer Ricciotti [Tue, 15 Jan 2008 14:38:50 +0000 (14:38 +0000)]
update: upper bound for prim

16 years agomore lemmas, til 3.26
Enrico Tassi [Mon, 14 Jan 2008 17:02:46 +0000 (17:02 +0000)]
more lemmas, til 3.26

16 years agonew deps
Enrico Tassi [Mon, 14 Jan 2008 16:37:39 +0000 (16:37 +0000)]
new deps

16 years agofirst lemma
Enrico Tassi [Mon, 14 Jan 2008 15:20:51 +0000 (15:20 +0000)]
first lemma

16 years agofixed a pulback and proved 3.17
Enrico Tassi [Mon, 14 Jan 2008 14:58:26 +0000 (14:58 +0000)]
fixed a pulback and proved 3.17

16 years agoadded some doc
Enrico Tassi [Mon, 14 Jan 2008 10:05:45 +0000 (10:05 +0000)]
added some doc

16 years agouser time is now printed correctly
Enrico Tassi [Mon, 14 Jan 2008 09:03:13 +0000 (09:03 +0000)]
user time is now printed correctly

16 years agobetter parsing of the root file
Enrico Tassi [Mon, 14 Jan 2008 09:03:01 +0000 (09:03 +0000)]
better parsing of the root file

16 years agofixed uris
Enrico Tassi [Mon, 14 Jan 2008 09:02:41 +0000 (09:02 +0000)]
fixed uris

16 years agoChebyshev's upper bound on prim
Wilmer Ricciotti [Mon, 14 Jan 2008 07:43:37 +0000 (07:43 +0000)]
Chebyshev's upper bound on prim

16 years agoremoved path for contribs
Enrico Tassi [Fri, 11 Jan 2008 19:13:29 +0000 (19:13 +0000)]
removed path for contribs

16 years agoadded a warning when a file is not compiled cause its buri is readonly
Enrico Tassi [Fri, 11 Jan 2008 19:11:09 +0000 (19:11 +0000)]
added a warning when a file is not compiled cause its buri is readonly

16 years agoMake does not even try to build files that would be compiled in read-only
Enrico Tassi [Fri, 11 Jan 2008 19:05:05 +0000 (19:05 +0000)]
Make does not even try to build files that would be compiled in read-only
baseuris

16 years agoI'll talk again with ferruccio, for the moment this is the right
Enrico Tassi [Fri, 11 Jan 2008 16:13:49 +0000 (16:13 +0000)]
I'll talk again with ferruccio, for the moment this is the right
way to allow every user that does and svn co to compile everithing.

16 years agoanother fix to make it more resistant
Enrico Tassi [Fri, 11 Jan 2008 15:52:06 +0000 (15:52 +0000)]
another fix to make it more resistant

16 years agomany sed to use notation for rewriting
Enrico Tassi [Fri, 11 Jan 2008 15:37:11 +0000 (15:37 +0000)]
many sed to use notation for rewriting

16 years ago.opt before .byte
Enrico Tassi [Fri, 11 Jan 2008 15:16:10 +0000 (15:16 +0000)]
.opt before .byte

16 years agougly hack to make matitac not exit when called on a readonly baseuri, but just fail
Enrico Tassi [Fri, 11 Jan 2008 15:15:38 +0000 (15:15 +0000)]
ugly hack to make matitac not exit when called on a readonly baseuri, but just fail

16 years agoadded a warning if the baseuri we want to clean is read-only
Enrico Tassi [Fri, 11 Jan 2008 15:08:45 +0000 (15:08 +0000)]
added a warning if the baseuri we want to clean is read-only

16 years ago-dot fixed, now the .dot file contains also edges
Enrico Tassi [Fri, 11 Jan 2008 14:59:19 +0000 (14:59 +0000)]
-dot fixed, now the .dot file contains also edges

16 years agoincreased timout
Enrico Tassi [Fri, 11 Jan 2008 14:10:06 +0000 (14:10 +0000)]
increased timout

16 years agoremoved useless assertion
Enrico Tassi [Fri, 11 Jan 2008 13:51:04 +0000 (13:51 +0000)]
removed useless assertion

16 years agoincreased a timeout, matitac (not .opt) should be able to do it in time
Enrico Tassi [Fri, 11 Jan 2008 10:25:29 +0000 (10:25 +0000)]
increased a timeout, matitac (not .opt) should be able to do it in time

16 years agoadded Sys.catch_break true
Enrico Tassi [Fri, 11 Jan 2008 10:24:53 +0000 (10:24 +0000)]
added Sys.catch_break true

16 years agocache for mtime of files is not polluted with None, minimal speedup
Enrico Tassi [Fri, 11 Jan 2008 09:58:41 +0000 (09:58 +0000)]
cache for mtime of files is not polluted with None, minimal speedup

16 years agoMake was caching too much, thus some targets were not rebuild properly
Enrico Tassi [Fri, 11 Jan 2008 09:52:46 +0000 (09:52 +0000)]
Make was caching too much, thus some targets were not rebuild properly

16 years agoBIG FAT WARNING: DEVELOPMENTS DIE HERE
Enrico Tassi [Thu, 10 Jan 2008 22:32:03 +0000 (22:32 +0000)]
BIG FAT WARNING: DEVELOPMENTS DIE HERE
What follows is the email on the helm mailing list

Riassunto:

 - non esistono più i developments

 - non esiste più il comando set "baseuri" "cic:/...." (non serve più)

 - questa mail è parecchio lunga, ma le prossime 2 sezioni le consiglio
   a _tutti_, quelle successive solo a chi aveva molti development
   dipendenti luno dall'altro. Ad ogni modo, il manuale di matita (che
   si apre con F1) è stato aggiornato e al posto dei developments ora
   spiega come funziona ora la compilazione.

Dove sono scritte le baseuri?

 - nella radice dei vostri ma (per esempio library/, tests/,
   contribs/RELATIOANL etc...) c'è un file di testo chiamato 'root'.

 - ad esempio il file library/root contiene una riga tipo:

       baseuri = cic:/matita

 - la baseuri in cui i files .ma vengono compilati si calcola guardando
   il path tra la radice e il file. As esempio

       library/nat/plus.ma

   essendo "radicato" da library/root che definisce la baseuri a
   cic:/matita verrà compilato in

       cic:/matita + /nat/plus/

   (esattamente dove era compilato prima, e tutti i .ma committati,
   quando necessario, sono stati porati a questo schema. In tutta
   library solo 1 file non lo rispettava).

Come si compila adesso che non c'è più matitamake?

 - da matita non cambia nulla, ho solo tolto un paio di popup che
   chiedevano sempre conferme di cose inutili (tipo se compilare il file
   incluso o no... ora lo compila sempre).

 - matitac ha cambiato leggermente semantica, ma potete fregarvene: la
   seguente linea continua a funzionare e fa le stesse cose di prima.

     cd library; make opt

 - il file delle dipendenze tra i files .ma prima veniva generato a ogni
   make con matitadep, ora non viene più fatto, quindi se cambiare gli
   includes che fate in un file fate un make depend.opt (o make depend
   se avete compilato in bytecode).

   matitadep è sempre stato lento, per questo motivo non viene chiamato
   tutte le volte. stamattina ho risolto un vecchissimo problema
   (ricordate che ogni tanto andava in stack overflow?) e ora mi sembra
   anche molto più veloce, quindi forse lo si potrebbe lanciare sempre
   ... vedremo

Qui finisce la parte necessaria a tutti, ci si sente coraggioso continui
pure. In generale il codice ML è diventato più semplice, matita è anche
più veloce a compilare e spero che i vari BUG dei developments siano
spariti. Chiaramente ce ne saranno di nuovi... ma spero di meno.

Dettagli del root file (dipendenze tra radici)

  - il root file è una lista associative chiave -> valore le cui linee
    matchano la seguente regexp:

      \s*[^=]+\s*=\s*.+\s*

    le chiavi utilizzabili sono: baseuri, include_paths.

  - per esempio, tests/ ha bisogno di legacy/ e vari files in tests/
    hanno la riga: include "coq.ma". Il root file per tests è:

        baseuri=cic:/tests
        include_paths=../legacy

  - library/ sta sempre negli include paths, se usate files in library
    non è necessario dichiarare il relativo include path

  - si possono dichiarare più include_paths, separandoli da spazi. per
    sempio

        include_paths=../foo ../../bar/baz

  - i files che includete devono esistere in uno degli include paths,
    e vengono cercati:

       - in / (path assoluto, da evitare possibilmente)
       - in .
       - in library/
       - negli include_paths

  - una volta scritto il root file, lanciando matitadep viene generato
    un file depends. Tale processo da anche degli errori, in caso alcuni
    files non riescano ad essere trovati nei paths specificati

  - una volta fatto ciò matita lanciato da dentro una radice compila
    tutto, quindi se serve "salta" in una delle radici specificate
    dagli include_paths e compila pure li dentro

  - non sono supportati (e non so nemmeno cosa voglia dire) files con lo
    stesso nome (e path relativo alla radice) in radici differenti,
    in tal caso include "a.ma" se a.ma esiste anche in una delle radici
    da cui si dipende, include sempre quello locale (prima c'era un bug
    per cui includeva quello non-locale). ho dovuto fare un po di
    renaming nei files di ferruccio, da capire se vanno bene.

Dove è finito make:

  - matitac ora legge il file depends e compila lui i files nell'orine
    giusto (e solo se necessario).

      ./matitac          compila tutto (nella radice della dir corrente)
      ./matitac foo/a.ma compila a.ma (e le sue dipendenze se necessario)

  - matitadep ha bisogno di un file root, detto ciò si cerca i files con
    estensione .ma e ne genera un depends, con formato:

      a b c
      b d
      d
      c

    le lettere sono nomi di files (quindi .ma, niente .moo, .mo,
    .mo.opt etc...). Le linee si leggono come

      a deve essere compilato dopo b e c
      b dopo d
      d e c anche subito

   i files esterni alla radice (trovati via include paths) vengono
   listati anche loro, senza dipendenze (tanto salta nella loro radice e
   fa "make" li dentro, dove le sue dipendenze sono note).

Mi sembra più veloce a compilare?!

 - prima, per ogni file .ma, veniva lanciato matitac, ora è lo stesso
   matitac a compilare tutti i files uno dopo l'altro. Il tempo speso a
   creare un processo (e per matita ce ne vuole parecchio) è
   risparmiato, quindi per un set di files molto piccoli si vede anche
   ad occhio la differenza.

 - il fatto che non venga generato un nuovo processo ha fatto si che
   tutti i bug relativi all'undo (parti imperative dello stato)
   venissero a galla. Ne è rimasto solo uno, che non so risolvere:
   quando camlp5 stampa "<W> una regola è stata mascherata" che li pare
   che tutto si inceppi.

 - il nostro environment è imperativo e nessuno lo svuota mai,
   risultato: non carica gli oggetti da disco quasi mai... è sia un bene
   che un male... potrei resettarlo alla fine di ogni comilazione...

 - Non ho mai provato a fare .ma con dipendenze circolari, magari diverge.

16 years agoimplementation of the make algorithm, still unfinished.
Enrico Tassi [Thu, 3 Jan 2008 10:13:04 +0000 (10:13 +0000)]
implementation of the make algorithm, still unfinished.
to be integrated with matitac to drop our beloved developments.

16 years ago* use findlib to pass -I flags down to ocamldoc, instead of relying on
Stefano Zacchiroli [Sat, 29 Dec 2007 20:05:54 +0000 (20:05 +0000)]
* use findlib to pass -I flags down to ocamldoc, instead of relying on
  hard-coded paths

16 years ago* bump standards-version, no changes needed
Stefano Zacchiroli [Sat, 29 Dec 2007 20:03:19 +0000 (20:03 +0000)]
* bump standards-version, no changes needed

16 years ago* convert the package to a non-native Debian package
Stefano Zacchiroli [Sat, 29 Dec 2007 20:02:29 +0000 (20:02 +0000)]
* convert the package to a non-native Debian package

16 years ago* debian/rules: instead of passing explicit -I flags to ocamldoc, do them
Stefano Zacchiroli [Fri, 28 Dec 2007 14:46:26 +0000 (14:46 +0000)]
* debian/rules: instead of passing explicit -I flags to ocamldoc, do them
  via ocamlfind and OCAML_OCAMLDOC_OCAMLFIND_FLAGS

16 years agooverwrite old symlink upon dist
Stefano Zacchiroli [Fri, 28 Dec 2007 14:44:09 +0000 (14:44 +0000)]
overwrite old symlink upon dist

16 years agoignore tons of generated stuff
Stefano Zacchiroli [Fri, 28 Dec 2007 14:22:55 +0000 (14:22 +0000)]
ignore tons of generated stuff

16 years ago* convert package to a non-native one (closes: #457353)
Stefano Zacchiroli [Fri, 28 Dec 2007 14:19:30 +0000 (14:19 +0000)]
* convert package to a non-native one (closes: #457353)

16 years ago* promote Vcs-* fields to real debian/control fields
Stefano Zacchiroli [Fri, 28 Dec 2007 14:12:38 +0000 (14:12 +0000)]
* promote Vcs-* fields to real debian/control fields
* update standards-version, no changes needed

16 years agobeginning proof of chebyshev's bound on prim.
Wilmer Ricciotti [Fri, 21 Dec 2007 16:09:59 +0000 (16:09 +0000)]
beginning proof of chebyshev's bound on prim.

16 years agoaccepts the poly shape for gviz maps
Enrico Tassi [Wed, 19 Dec 2007 15:10:19 +0000 (15:10 +0000)]
accepts the poly shape for gviz maps

16 years agoupper bound for logarithmic summation
Wilmer Ricciotti [Mon, 17 Dec 2007 21:31:35 +0000 (21:31 +0000)]
upper bound for logarithmic summation

16 years agoA few more lemmas.
Andrea Asperti [Mon, 17 Dec 2007 12:07:27 +0000 (12:07 +0000)]
A few more lemmas.

16 years agoMuch more verbose statistics.
Claudio Sacerdoti Coen [Sun, 16 Dec 2007 15:12:10 +0000 (15:12 +0000)]
Much more verbose statistics.

16 years agoBug fixed: \n prevented recognition.
Claudio Sacerdoti Coen [Sun, 16 Dec 2007 14:19:01 +0000 (14:19 +0000)]
Bug fixed: \n prevented recognition.

16 years agoSome inequalities.
Andrea Asperti [Thu, 13 Dec 2007 15:29:58 +0000 (15:29 +0000)]
Some inequalities.

16 years agoProgress.
Wilmer Ricciotti [Wed, 12 Dec 2007 18:26:29 +0000 (18:26 +0000)]
Progress.

16 years agoadd support for adding identifiers instead of only changing them (enabled per default)
Stefano Zacchiroli [Wed, 12 Dec 2007 18:13:14 +0000 (18:13 +0000)]
add support for adding identifiers instead of only changing them (enabled per default)

16 years agoPartial progress.
Andrea Asperti [Tue, 11 Dec 2007 15:26:48 +0000 (15:26 +0000)]
Partial progress.

16 years agomore chosmetic
Enrico Tassi [Mon, 10 Dec 2007 14:49:59 +0000 (14:49 +0000)]
more chosmetic

16 years agoMain result for e.
Andrea Asperti [Mon, 10 Dec 2007 14:24:40 +0000 (14:24 +0000)]
Main result for e.

16 years agosandeich lemma makeup
Enrico Tassi [Mon, 10 Dec 2007 11:39:38 +0000 (11:39 +0000)]
sandeich lemma makeup

16 years agoRestructuring.
Andrea Asperti [Mon, 10 Dec 2007 10:11:13 +0000 (10:11 +0000)]
Restructuring.

16 years agoMain inequalities for e.
Andrea Asperti [Mon, 10 Dec 2007 08:43:07 +0000 (08:43 +0000)]
Main inequalities for e.

16 years agoAdded summation formula for the power of a binomial.
Wilmer Ricciotti [Sun, 9 Dec 2007 23:28:01 +0000 (23:28 +0000)]
Added summation formula for the power of a binomial.

16 years agothe is_structure is a bad idea if you don't have canonical structures.
Enrico Tassi [Sat, 8 Dec 2007 10:36:00 +0000 (10:36 +0000)]
the is_structure is a bad idea if you don't have canonical structures.

16 years agoBinomial coefficients and costant e.
Andrea Asperti [Fri, 7 Dec 2007 11:41:49 +0000 (11:41 +0000)]
Binomial coefficients and costant e.

16 years agoA few more theorems.
Andrea Asperti [Fri, 7 Dec 2007 11:38:57 +0000 (11:38 +0000)]
A few more theorems.