--- a/src/HOL/Nitpick.thy Fri Jun 11 16:34:56 2010 +0200
+++ b/src/HOL/Nitpick.thy Fri Jun 11 17:05:11 2010 +0200
@@ -214,6 +214,10 @@
definition inverse_frac :: "'a \<Rightarrow> 'a" where
"inverse_frac q \<equiv> frac (denom q) (num q)"
+definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+[nitpick_simp]:
+"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
+
definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
[nitpick_simp]:
"less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
@@ -245,7 +249,7 @@
wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
- less_eq_frac of_frac
+ less_frac less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
@@ -254,6 +258,6 @@
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_eq_frac_def of_frac_def
+ inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
end