src/HOL/Nonstandard_Analysis/HyperNat.thy
changeset 67091 1393c2340eec
parent 64438 f91cae6c1d74
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
     1.5    by transfer simp
     1.6  
     1.7 -lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
     1.8 +lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d \<longrightarrow> d \<in> range of_nat"
     1.9    apply (induct n)
    1.10     apply (auto simp add: add.assoc)
    1.11    apply (case_tac x)