src/FOLP/ex/Intro.thy
changeset 58889 5b7a9633cfa8
parent 41526 54b4686704af
child 58957 c9e744ea8a38
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     3     Copyright   1992  University of Cambridge
     3     Copyright   1992  University of Cambridge
     4 
     4 
     5 Derives some inference rules, illustrating the use of definitions.
     5 Derives some inference rules, illustrating the use of definitions.
     6 *)
     6 *)
     7 
     7 
     8 header {* Examples for the manual ``Introduction to Isabelle'' *}
     8 section {* Examples for the manual ``Introduction to Isabelle'' *}
     9 
     9 
    10 theory Intro
    10 theory Intro
    11 imports FOLP
    11 imports FOLP
    12 begin
    12 begin
    13 
    13