1 theory Base

     1 theory Base

     2 imports Main 

     2 imports Main 

     3         "~~/src/HOL/Library/LaTeXsugar"

     3         "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     4 begin

     5 

     6 

     6 notation (latex output)

     7 notation (latex output)

     7   Cons ("_ # _" [66,65] 65)

     8   Cons ("_ # _" [66,65] 65)

     8 

     9 

     9 ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 

    10 ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)