src/HOL/Quickcheck_Narrowing.thy
changeset 43378 d7ae1fae113b
parent 43356 2dee03f192b7
child 43542 7e2ef426c960
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Jun 13 23:21:53 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Tue Jun 14 08:30:18 2011 +0200
     1.3 @@ -207,14 +207,6 @@
     1.4  subsubsection {* Narrowing's deep representation of types and terms *}
     1.5  
     1.6  datatype narrowing_type = SumOfProd "narrowing_type list list"
     1.7 -text {*
     1.8 -The definition of the automatically derived equal type class instance for @{typ narrowing_type}
     1.9 -causes an error in the OCaml serializer.
    1.10 -For the moment, we delete this equation manually because we do not require an executable equality
    1.11 -on this type anyway.   
    1.12 -*}
    1.13 -declare Quickcheck_Narrowing.equal_narrowing_type_def[code del]
    1.14 -
    1.15  datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
    1.16  datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
    1.17