changeset 17472 | bcbf48d59059 |
parent 17085 | 5b57f995a179 |
child 19601 | 299d4cd2ef51 |
--- a/src/HOL/Integ/IntArith.thy Sat Sep 17 18:24:57 2005 +0200 +++ b/src/HOL/Integ/IntArith.thy Sat Sep 17 18:25:11 2005 +0200 @@ -226,7 +226,7 @@ done -subsubsection "Induction principles for int" +subsection "Induction principles for int" (* `set:int': dummy construction *) theorem int_ge_induct[case_names base step,induct set:int]: