[Hol-info] HOL Workshop 2016: Final call

Thinking of submitting an abstract for the HOL workshop this year? They are due tomorrow! It's easy to write one. Don't miss out :) See the call below. --- CALL FOR ABSTRACTS 2016 International Workshop on the HOL Theorem Proving System

Re: [Hol-info] Is there a function that can produce random number in HOL4?

Hi Ada, could you explain in more detail what you want? I did not get wether you need in ML or in the logic. Moreover, I did not get the "x = ..." part. In ML, look at the structure "Random". In the logic such a function cannot exists, since forall f, args "f args = f args" holds, which would

[Hol-info] Is there a function that can produce random number in HOL4?

Hi,guys I am working with HOL4. Now, I need a function that can produce random number. For example, supposing that function rand can create a random number, then x=rand ()/LENGTH, where x is a number between 1 and LENGTH. Does anyone know this?