changeset 1366 3f3c25d3ec04 parent 1185 9968989790e2 child 1387 9bcad9c22fd4
equal inserted replaced
1365:0defae128e43 1366:3f3c25d3ec04
   435 defs    nand_def "nand(P,Q) == ~(P & Q)"
   435 defs    nand_def "nand(P,Q) == ~(P & Q)"
   436         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   436         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   437 end
   437 end
   438 \end{ttbox}
   438 \end{ttbox}
   439
   439

   440 \begin{warn}

   441 A common mistake when writing definitions is to introduce extra free variables

   442 on the right-hard side as in the following fictitious definition:

   443 \begin{ttbox}

   444 defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"

   445 \end{ttbox}

   446 Isabelle rejects this definition'' because of the extra {\tt m} on the

   447 right-hard side, which would introduce an inconsistency. What you should have

   448 written is

   449 \begin{ttbox}

   450 defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"

   451 \end{ttbox}

   452 \end{warn}
   440
   453
   441 \subsection{Declaring type constructors}
   454 \subsection{Declaring type constructors}
   442 \indexbold{types!declaring}\indexbold{arities!declaring}
   455 \indexbold{types!declaring}\indexbold{arities!declaring}
   443 %
   456 %
   444 Types are composed of type variables and {\bf type constructors}.  Each
   457 Types are composed of type variables and {\bf type constructors}.  Each