[isabelle] Proof failed for datatype



Hi all,

As far as I can tell, I seem to have run into an issue with the datatype 
package. After slightly increasing the complexity of an existing 
datatype I get a 'Proof failed' error message.

The problematic datatype is
datatype ('s, 'p) test' =
    Test' "(('s, 'p) test' à 's set à 's set) list"

Cheers,
Corey



theory Test
imports Main
begin

datatype 's test =
  Test "('s test \<times> 's set \<times> 's set) list"

datatype ('s, 'p) test' =
  Test' "(('s, 'p) test' \<times> 's set \<times> 's set) list"

end


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