src/HOL/ex/Cartouche_Examples.thy
changeset 59089 da2fef2faa83
parent 59068 8606f2ee11b1
child 59112 e670969f34df
equal deleted inserted replaced
59088:ff2bd4a14ddb 59089:da2fef2faa83
       
     1 (*  Title:      HOL/ex/Cartouche_Examples.thy
       
     2     Author:     Makarius
       
     3 *)
       
     4 
     1 section \<open>Some examples with text cartouches\<close>
     5 section \<open>Some examples with text cartouches\<close>
     2 
     6 
     3 theory Cartouche_Examples
     7 theory Cartouche_Examples
     4 imports Main
     8 imports Main
     5 keywords
     9 keywords