dropped dead code
authorhaftmann
Sun Oct 08 22:28:19 2017 +0200 (19 months ago)
changeset 66795420d0080545f
parent 66794 83bf64da6938
child 66796 ea9b2e5ca9fc
dropped dead code
src/HOL/Nat_Transfer.thy
src/HOL/Tools/legacy_transfer.ML
     1.1 --- a/src/HOL/Nat_Transfer.thy	Mon Oct 09 16:14:18 2017 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4      "(int x) * (int y) = int (x * y)"
     1.5      "tsub (int x) (int y) = int (x - y)"
     1.6      "(int x)^n = int (x^n)"
     1.7 -  by (auto simp add: of_nat_mult tsub_def of_nat_power)
     1.8 +  by (auto simp add: tsub_def)
     1.9  
    1.10  lemma transfer_int_nat_function_closures:
    1.11      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
     2.1 --- a/src/HOL/Tools/legacy_transfer.ML	Mon Oct 09 16:14:18 2017 +0100
     2.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Sun Oct 08 22:28:19 2017 +0200
     2.3 @@ -154,7 +154,6 @@
     2.4      { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 }
     2.5      { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
     2.6    let
     2.7 -    fun add_del eq del add = union eq add #> subtract eq del;
     2.8      val guessed = if guess
     2.9        then map (fn thm => transfer_thm
    2.10          ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1