src/HOL/Library/RBT_Set.thy
changeset 55565 f663fc1e653b
parent 54263 c4159fe6fa46
child 55584 a879f14b6f95
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Feb 18 23:03:49 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Feb 18 23:03:50 2014 +0100
     1.3 @@ -423,7 +423,7 @@
     1.4  (** abstract **)
     1.5  
     1.6  lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
     1.7 -  is rbt_fold1_keys by simp
     1.8 +  is rbt_fold1_keys .
     1.9  
    1.10  lemma fold1_keys_def_alt:
    1.11    "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
    1.12 @@ -441,9 +441,9 @@
    1.13  
    1.14  (* minimum *)
    1.15  
    1.16 -lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
    1.17 +lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
    1.18  
    1.19 -lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
    1.20 +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
    1.21  
    1.22  lemma r_min_alt_def: "r_min t = fold1_keys min t"
    1.23  by transfer (simp add: rbt_min_def)
    1.24 @@ -479,9 +479,9 @@
    1.25  
    1.26  (* maximum *)
    1.27  
    1.28 -lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
    1.29 +lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
    1.30  
    1.31 -lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
    1.32 +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
    1.33  
    1.34  lemma r_max_alt_def: "r_max t = fold1_keys max t"
    1.35  by transfer (simp add: rbt_max_def)