Eric Hall

Defining multiple independent functions in the same definition block.

4

It would be good to be able to tell HOL to allow you to define multiple independent functions in one definition block without it complaining, because this would make it...

I have attached an example file which explains what I mean (rename it from a .txt file to a .sml file, had to name it that way because it won't...

If I have the following code: ``` open HolKernel Parse boolLib bossLib; Definition foo_def: foo (x : num) = ARB End Theorem foo_two = SPEC “2 : num” foo_def; (*...