src/HOL/Proofs/Lambda/Eta.thy
changeset 58273 9f0bfcd15097
parent 47124 960f0a4404c7
child 58622 aa99568f56de
equal deleted inserted replaced
58272:61d94335ef6c 58273:9f0bfcd15097
   179     "(\<not> free s i) = (\<exists>t. s = lift t i)"
   179     "(\<not> free s i) = (\<exists>t. s = lift t i)"
   180   apply (induct s arbitrary: i)
   180   apply (induct s arbitrary: i)
   181     apply simp
   181     apply simp
   182     apply (rule iffI)
   182     apply (rule iffI)
   183      apply (erule linorder_neqE)
   183      apply (erule linorder_neqE)
   184       apply (rule_tac x = "Var nat" in exI)
   184       apply (rename_tac nat a, rule_tac x = "Var nat" in exI)
   185       apply simp
   185       apply simp
   186      apply (rule_tac x = "Var (nat - 1)" in exI)
   186      apply (rename_tac nat a, rule_tac x = "Var (nat - 1)" in exI)
   187      apply simp
   187      apply simp
   188     apply clarify
   188     apply clarify
   189     apply (rule notE)
   189     apply (rule notE)
   190      prefer 2
   190      prefer 2
   191      apply assumption
   191      apply assumption