doc-src/TutorialI/Recdef/examples.thy
changeset 16417 9bc16273c2d4
parent 15905 0a4cc9b113c7
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     1 (*<*)
     1 (*<*)
     2 theory examples = Main:;
     2 theory examples imports Main begin;
     3 (*>*)
     3 (*>*)
     4 
     4 
     5 text{*
     5 text{*
     6 Here is a simple example, the \rmindex{Fibonacci function}:
     6 Here is a simple example, the \rmindex{Fibonacci function}:
     7 *}
     7 *}