src/HOL/MetisExamples/BT.thy
changeset 31790 05c92381363c
parent 29782 02e76245e5af
child 32864 a226f29d4bdc
     1.1 --- a/src/HOL/MetisExamples/BT.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/MetisExamples/BT.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4  ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
     1.5  lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
     1.6    apply (induct t)
     1.7 -  apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
     1.8 +  apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
     1.9    apply (metis bt_map.simps(2) n_leaves.simps(2))
    1.10    done
    1.11