src/HOL/ex/Eval_Examples.thy
changeset 30240 5b25fee0362c
parent 28952 15a4b2cf8c34
child 32067 e425fe0ff24a
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
     1 (*  ID:         $Id$
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2     Author:     Florian Haftmann, TU Muenchen
       
     3 *)
       
     4 
     2 
     5 header {* Small examples for evaluation mechanisms *}
     3 header {* Small examples for evaluation mechanisms *}
     6 
     4 
     7 theory Eval_Examples
     5 theory Eval_Examples
     8 imports Code_Eval Rational
     6 imports Code_Eval Rational