src/HOL/Decision_Procs/ferrack_tac.ML
changeset 31790 05c92381363c
parent 31302 12677a808d43
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  val split_zmod = @{thm split_zmod};
     1.5  val mod_div_equality' = @{thm mod_div_equality'};
     1.6  val split_div' = @{thm split_div'};
     1.7 -val Suc_plus1 = @{thm Suc_plus1};
     1.8 +val Suc_eq_plus1 = @{thm Suc_eq_plus1};
     1.9  val imp_le_cong = @{thm imp_le_cong};
    1.10  val conj_le_cong = @{thm conj_le_cong};
    1.11  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;