equal
deleted
inserted
replaced
443 on the right-hard side as in the following fictitious definition: |
443 on the right-hard side as in the following fictitious definition: |
444 \begin{ttbox} |
444 \begin{ttbox} |
445 defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)" |
445 defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)" |
446 \end{ttbox} |
446 \end{ttbox} |
447 Isabelle rejects this ``definition'' because of the extra {\tt m} on the |
447 Isabelle rejects this ``definition'' because of the extra {\tt m} on the |
448 right-hard side, which would introduce an inconsistency. What you should have |
448 right-hand side, which would introduce an inconsistency. What you should have |
449 written is |
449 written is |
450 \begin{ttbox} |
450 \begin{ttbox} |
451 defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)" |
451 defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)" |
452 \end{ttbox} |
452 \end{ttbox} |
453 \end{warn} |
453 \end{warn} |