Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-17 11:24:43 -0800 (Mon, 17 Nov 2003)
Revision: 5107
Log message:
Added Mark's theory of messages automata from Nuprl.
Mark and me transfered Nuprl theories (at least basic ones used by message
automata system) into MetaPRL.
We did theorems, definitions, and display forms.
mesa/nuprl_* theories are generated from nuprl.
Some theorems could be stated as better MetaPRL rules.
we add such theorems in mesa/ma_* theories to avoid conflicts in the case if
we want to regenerate Nuprl theories.
The dependency is the following:
Ma_(theory) depends on Nuprl_(theory) and
Nuprl_(theory) depends on Ma_(previous theory)
Eventually all Nuprl stuff should go to appropriate place in Itt.
(Some stuff is already their).