equal
deleted
inserted
replaced
344 THEN ALLGOALS (asm_full_simp_tac simp_set) |
344 THEN ALLGOALS (asm_full_simp_tac simp_set) |
345 end |
345 end |
346 |
346 |
347 (* simpset for size goals *) |
347 (* simpset for size goals *) |
348 val size_simpset = HOL_ss |
348 val size_simpset = HOL_ss |
349 addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
349 addsimprocs [@{simproc natless_cancel_numerals}] |
350 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
350 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
351 zero_less_Suc prod.size(1) mult_Suc_right} |
351 zero_less_Suc prod.size(1) mult_Suc_right} |
352 |
352 |
353 val natT = @{typ nat} |
353 val natT = @{typ nat} |
354 |
354 |