From 65346b3f0a548fc07241a2ac9e53506f5634ee7c Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 8 Feb 2019 15:43:49 +0100
Subject: [PATCH] kleinkram

---
 examples/conceptual/Attributes.thy | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy
index eacb904..4378a73 100644
--- a/examples/conceptual/Attributes.thy
+++ b/examples/conceptual/Attributes.thy
@@ -17,6 +17,12 @@ Symtab.dest docitem_tab;
 Symtab.dest docclass_tab;
 \<close>
 
+ML\<open>
+fun fac x = if x = 0 then 1 else x * (fac(x -1));
+fac 3;
+open Thm;
+\<close>
+
 text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
 text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ...  @{thm refl} \<close>