# HG changeset patch # User huffman # Date 1333110449 -7200 # Node ID 4fc34c62847440519ccebc59e188de36596fa789 # Parent 1b7c909a6fadb208245919e7b99b2a61e09193c2 remove content-free theory ex/Arithmetic_Series_Complex.thy diff -r 1b7c909a6fad -r 4fc34c628474 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 30 14:25:32 2012 +0200 +++ b/src/HOL/IsaMakefile Fri Mar 30 14:27:29 2012 +0200 @@ -1128,7 +1128,7 @@ Library/Code_Integer.thy Library/Code_Nat.thy \ Library/Code_Natural.thy Library/Efficient_Nat.thy \ Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ - ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ + ex/Arith_Examples.thy ex/BT.thy \ ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \ ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \ ex/Code_Nat_examples.thy \ diff -r 1b7c909a6fad -r 4fc34c628474 src/HOL/ex/Arithmetic_Series_Complex.thy --- a/src/HOL/ex/Arithmetic_Series_Complex.thy Fri Mar 30 14:25:32 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: HOL/ex/Arithmetic_Series_Complex.thy - Author: Benjamin Porter, 2006 -*) - - -header {* Arithmetic Series for Reals *} - -theory Arithmetic_Series_Complex -imports "../RealDef" -begin - -lemma arith_series_real: - "(2::real) * (\i\{..