# HG changeset patch # User haftmann # Date 1457609581 -3600 # Node ID 7011429f44f98e4048e70ef71d785f3057f37ceb # Parent bfa38c2e751fd25e8097c28f7b8ff3b311ebfeae moved diff -r bfa38c2e751f -r 7011429f44f9 src/HOL/List.thy --- a/src/HOL/List.thy Wed Mar 09 21:01:22 2016 +0100 +++ b/src/HOL/List.thy Thu Mar 10 12:33:01 2016 +0100 @@ -3006,6 +3006,14 @@ lemma upt_conv_Cons: "i < j ==> [i..no precondition\ + "m # n # ns = [m.. n # ns = [Suc m.. [i.. \LOOPS as a simprule, since \j <= j\.\ by (induct k) auto diff -r bfa38c2e751f -r 7011429f44f9 src/HOL/String.thy --- a/src/HOL/String.thy Wed Mar 09 21:01:22 2016 +0100 +++ b/src/HOL/String.thy Thu Mar 10 12:33:01 2016 +0100 @@ -6,15 +6,6 @@ imports Enum begin -lemma upt_conv_Cons_Cons: -- \no precondition\ -- \FIXME move\ - "m # n # ns = [m.. n # ns = [Suc m..Characters and strings\ subsubsection \Characters as finite algebraic type\