| changeset 49070 | f00fee6d21d4 |
| parent 48891 | c0eafbd55de3 |
| child 49962 | a8cc904a6820 |
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Sep 03 09:15:40 2012 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Sep 03 09:15:58 2012 +0200 @@ -2013,19 +2013,16 @@ lemma fixes x :: real shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1" -apply rferrack -done + by rferrack lemma fixes x :: real shows "\<exists>y \<le> x. x = y + 1" -apply rferrack -done + by rferrack lemma fixes x :: real shows "\<not> (\<exists>z. x + z = x + z + 1)" -apply rferrack -done + by rferrack end