equal
deleted
inserted
replaced
918 in simp_depth := depth; |
918 in simp_depth := depth; |
919 bottomc (mode, prover, sign, maxidx) mss ct |
919 bottomc (mode, prover, sign, maxidx) mss ct |
920 end |
920 end |
921 handle THM (s, _, thms) => |
921 handle THM (s, _, thms) => |
922 error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^ |
922 error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^ |
923 Pretty.string_of (pretty_thms thms)); |
923 Pretty.string_of (Display.pretty_thms thms)); |
924 |
924 |
925 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) |
925 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) |
926 (*Do not rewrite flex-flex pairs*) |
926 (*Do not rewrite flex-flex pairs*) |
927 fun goals_conv pred cv = |
927 fun goals_conv pred cv = |
928 let fun gconv i ct = |
928 let fun gconv i ct = |