equal
deleted
inserted
replaced
646 | mutthmrec (x::xs) = |
646 | mutthmrec (x::xs) = |
647 let |
647 let |
648 val mutated = mutate option (prop_of x) usedthy |
648 val mutated = mutate option (prop_of x) usedthy |
649 commutatives forbidden_funs iter |
649 commutatives forbidden_funs iter |
650 val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter |
650 val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter |
651 val thmname = "\ntheorem " ^ (Thm.get_name x) ^ ":" |
651 val thmname = "\ntheorem " ^ Thm.get_name_hint x ^ ":" |
652 val pnumstring = string_of_int passednum |
652 val pnumstring = string_of_int passednum |
653 val cenumstring = string_of_int cenum |
653 val cenumstring = string_of_int cenum |
654 in |
654 in |
655 (File.append (Path.explode filename) |
655 (File.append (Path.explode filename) |
656 (thmname ^ (create_spaces thmname 50) ^ |
656 (thmname ^ (create_spaces thmname 50) ^ |