Hi Brian,
Our current policy is the Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
OK, the requirement for Plain I can understand. For Main, it doesn't
seem too unreasonable, assuming it's necessary (since most theory files
import Main anyway).
But
I completely agree with Brian (even I can not agree to import Main
instead of theories under Main).
There is only two things I can think of:
1) You can't be serious about this
2) We are all sitting back and watching how things get worse.
The bootstrap process of Main *was* fragile. For
Dear all,
I have a theory development which used to work not a long time ago. I am
now trying to include it into the distribution.
At some point I can not merge the theories and get:
*** Clash of specifications Permutations.typerep_^_inst.typerep_^_def
and Misc.typerep_^_inst.typerep_^_def
I've moved things up (although this is really artificial).
Misc imports Complex_Main anyway, and I made Permutations import Main,
the problem persists.
Florian Haftmann wrote:
Hi Amine,
I have a theory development which used to work not a long time ago. I am
now trying to include it into
Can you provide me with a theory graph of Permutations and Misc? (Isar
command thy_graph, export to ps/pdf)?
Florian
Amine Chaieb schrieb:
I've moved things up (although this is really artificial).
Misc imports Complex_Main anyway, and I made Permutations import Main,
the problem
Do you mean thy_deps? It's not working on my machine.
Can you do
cvs -d
haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co
work/Lib
The files are then under Multivariate.
Amine.
PS: Please forgive for still using cvs, but I am applying the first
commandment of Computer
Amine Chaieb schrieb:
Do you mean thy_deps? It's not working on my machine.
Yes, thy_deps of course (sorry for the slip). But thy doesn't it work?
cd lib/browser
make
should do the job...
Florian
Can you do
cvs -d
haftmann at
Florian Haftmann wrote:
Amine Chaieb schrieb:
Do you mean thy_deps? It's not working on my machine.
Yes, thy_deps of course (sorry for the slip). But thy doesn't it work?
cd lib/browser
make
should do the job...
Florian
Can you do
cvs -d
haftmann at
OK
Florian Haftmann wrote:
I have to bother you further:
it is necessary to unfold the [HOL] node in the graph (by clicking on
it) because we need to inspect the internal structure of the HOL theories.
Florian
Amine Chaieb schrieb:
Florian Haftmann wrote:
Amine Chaieb schrieb:
OK, seems like you have to change the following:
a) add Fact to the imports of Plain
b) add Main to the imports of Infinite_Set
and to the imports of Finite_Cartesian_Products
Our current policy is the Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
Hope this
and the fishing rules...
Our current policy is that Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
But feel free to ask if this is still obscure.
This rule does not tell me anything since it is trivally satisfied by
any connected graph containing
Our current policy is that Plain, Main (and Complex_Main) are either
ancestors or descendants of any theory.
This rule does not tell me anything since it is trivally satisfied by
any connected graph containing Plain, Main and Complex_Main.
The rule rules out the following situation:
A
12 matches
Mail list logo
