theory Base+
−
imports Main +
−
        "~~/src/HOL/Library/LaTeXsugar"+
−
begin+
−
+
−
print_ML_antiquotations+
−
+
−
text \<open>Hallo ML Antiquotation:+
−
@{ML \<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"+
−
ML_file "antiquote_setup.ML"+
−
+
−
+
−
(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)+
−
setup {* AntiquoteSetup.setup *}+
−
+
−
print_ML_antiquotations+
−
+
−
text \<open>Hallo ML Antiquotation:+
−
@{ML \<open>2 + 3\<close> }+
−
\<close>+
−
+
−
end+
−