[isabelle-dev] Typerep again
florian.haftmann at informatik.tu-muenchen.de
Mon Feb 9 15:58:32 CET 2009
> Please do not give me fish but teach me how to fish!
Hmmm... I had been thinking I was doing both:
>> 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
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.
P.S. Hopefully we are not in the small village with the crazy people
where always conflicts arise as soon as the matter of fish is discussed...
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev