theory Base
imports Main 
        "~~/src/HOL/Library/LaTeXsugar"
begin

ML \<open>@{assert} true\<close>
ML \<open>@{print} (2 + 3 +4)\<close>


print_ML_antiquotations
text \<open>
Can we put an ML-val into the text?

@{ML [display] \<open>2 + 3\<close>}

\<close>
notation (latex output)
  Cons ("_ # _" [66,65] 65)

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

fun rhs 1 = P 1
  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))

fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 
                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)

fun de_bruijn n =
  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}

ML_file "output_tutorial.ML"
text \<open>
Can we put an ML-val into the text?

@{ML [gray] \<open>2 + 3\<close>}
\<close>

ML_file "antiquote_setup.ML"


(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
setup {* AntiquoteSetup.setup *}


end