| changeset 56107 | 2ec2d06b9424 |
| parent 56103 | 6689512f3710 |
| child 57156 | 3546a67226ea |
--- a/src/HOL/SMT2.thy Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/SMT2.thy Thu Mar 13 14:48:20 2014 +0100 @@ -90,7 +90,7 @@ lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" by simp -lemma nat_int: "\<forall>n. nat (int n) = n" by simp +lemma nat_int': "\<forall>n. nat (int n) = n" by simp lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp