1 theory Prove

     1 theory Prove

     3 begin

     3 begin

     4 

     4 

     5 ML {*

     5 ML {*

     6 val r = Unsynchronized.ref (NONE:(unit -> term) option)

     6 val r = Unsynchronized.ref (NONE:(unit -> term) option)

     7 *}

     7 *}