# HG changeset patch
# User paulson
# Date 1114612799 -7200
# Node ID cf2c6cf35216925441e13998b1e951825e3d3bd9
# Parent  a344c4284972440dbdef8aad83eb3848d027ea51
tidied

diff -r a344c4284972 -r cf2c6cf35216 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Wed Apr 27 16:39:44 2005 +0200
+++ b/src/HOL/NatArith.thy	Wed Apr 27 16:39:59 2005 +0200
@@ -132,8 +132,6 @@
 
 ML
 {*
-val nat_diff_split = thm "nat_diff_split";
-val nat_diff_split_asm = thm "nat_diff_split_asm";
 val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
 val nat_diff_split = thm "nat_diff_split";
 val nat_diff_split_asm = thm "nat_diff_split_asm";