src/HOL/Nat.thy
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 *}