doc-src/TutorialI/Misc/Itrev.thy
changeset 16417 9bc16273c2d4
parent 15905 0a4cc9b113c7
child 17326 9fe23a5bb021
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     1 (*<*)
     1 (*<*)
     2 theory Itrev = Main:;
     2 theory Itrev imports Main begin;
     3 (*>*)
     3 (*>*)
     4 
     4 
     5 section{*Induction Heuristics*}
     5 section{*Induction Heuristics*}
     6 
     6 
     7 text{*\label{sec:InductionHeuristics}
     7 text{*\label{sec:InductionHeuristics}