src/HOL/Import/HOL/arithmetic.imp
changeset 33657 a4179bf442d1
parent 31790 05c92381363c
child 34974 18b41bba42b5
equal deleted inserted replaced
33648:555e5358b8c9 33657:a4179bf442d1
   189   "LESS_EQ_CASES" > "Nat.nat_le_linear"
   189   "LESS_EQ_CASES" > "Nat.nat_le_linear"
   190   "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
   190   "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
   191   "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
   191   "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
   192   "LESS_EQ_ADD" > "Nat.le_add1"
   192   "LESS_EQ_ADD" > "Nat.le_add1"
   193   "LESS_EQ_0" > "Nat.le_0_eq"
   193   "LESS_EQ_0" > "Nat.le_0_eq"
   194   "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
   194   "LESS_EQUAL_ANTISYM" > "Nat.le_antisym"
   195   "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
   195   "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
   196   "LESS_EQ" > "Nat.le_simps_3"
   196   "LESS_EQ" > "Nat.le_simps_3"
   197   "LESS_DIV_EQ_ZERO" > "Divides.div_less"
   197   "LESS_DIV_EQ_ZERO" > "Divides.div_less"
   198   "LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP"
   198   "LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP"
   199   "LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES"
   199   "LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES"