70 text{* 

    70 text{* 

    71   yields the expected result @{text 2}. Similarly we can prove that

    71   yields the expected result @{text 2}. Similarly we can prove that

    72   @{text 4} is not prime: 

    72   @{text 4} is not prime: 

    73 *}

    73 *}

    74 

    74 

    76   apply(rule factor_non_prime)

    76   apply(rule factor_non_prime)

    77   apply eval

    77   apply eval

    78   done

    78   done

    79 

    79 

    80 text{* 

    80 text{*