[isabelle] Questions about Isar


I want a function to return the number of the subgoals, how can I do it?
I find some functions, e.g. topthm(), can not work in Isar as in Isabelle. I wonder if it is worth making a lot of Isabelles running on different computers
concurrently to prove one goal cooperating with each other?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.