Continuing to answer my own questions ... I went back to Isabelle and found
that it has been evolving very nicely, and that very large scale proofs
about programs have been accomplished using it. One still has to know what
one is doing but it is no longer a matter of juggling chainsaws.
The Is
I think the reason for it is probably because Sage variables are so often
words rather than letters When using LaTeX directly on formulas involving
typical programming variable names one has to override the "carefully tuned
spacing" in just this way.
A patch to leave out the space when both si
I think the reason for it is probably because Sage variables are so often
words rather than letters. A patch to leave out the space when both sides
of a product are integer literals, single-letter variables or have
non-default (user defined) latex forms. When using LaTeX directly on
formulas
Apparently the answer to my last question is "yes". Since I originally
studied the Sage tutorials a couple of years ago "var" has been extended to
attache a domain to variables. Still reading up on it, it's connected to
the assumptions mechanism and simplify method. I used all of the above in
This forum is for the open-source mathematics program called Sage. You want
the commercial office automation software company called Sage. See sage.com.
--
You received this message because you are subscribed to the Google Groups
"sage-support" group.
To unsubscribe from this group and stop r
In graduate school I used Mathematica all day every day. I've not had the
luxury of that kind of immersion in Sage (yet). But I've searched the
documentation and the forums and I see others struggling with the same issue
I'm having so I don't think it's just me.
I am working on mathematical a
