doc-src/TutorialI/Misc/AdvancedInd.thy
changeset 16417 9bc16273c2d4
parent 12815 1f073030b97a
child 25258 22d16596c306
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     1 (*<*)
     1 (*<*)
     2 theory AdvancedInd = Main:;
     2 theory AdvancedInd imports Main begin;
     3 (*>*)
     3 (*>*)
     4 
     4 
     5 text{*\noindent
     5 text{*\noindent
     6 Now that we have learned about rules and logic, we take another look at the
     6 Now that we have learned about rules and logic, we take another look at the
     7 finer points of induction.  We consider two questions: what to do if the
     7 finer points of induction.  We consider two questions: what to do if the