[isabelle] Translating syntactic sugar


I was wondering how to translate

"\forall s in S. t(s)" into a let expression where t :: nat * nat.

let ?p = "ALL s. s : S --> t s < 0" isn't right since it has the type bool
=> bool, right? I'd want ?p to have the type nat, right?



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