| changeset 57983 | 6edc3529bb4e | 
| parent 57952 | 1a9a6dfc255f | 
| child 58189 | 9d714be4f028 | 
--- a/src/HOL/Nat.thy Mon Aug 18 15:03:25 2014 +0200 +++ b/src/HOL/Nat.thy Mon Aug 18 17:19:58 2014 +0200 @@ -132,9 +132,9 @@ nat.collapse nat.expand nat.sel - nat.sel_exhaust - nat.sel_split - nat.sel_split_asm + nat.exhaust_sel + nat.split_sel + nat.split_sel_asm lemma nat_exhaust [case_names 0 Suc, cases type: nat]: -- {* for backward compatibility -- names of variables differ *}