From be04e99c2f6445a1a553dac13ee14e3fff72b4ee Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 17 Apr 2018 15:24:19 +0200
Subject: [PATCH] Added little things in Idir example.

Just to show.
---
 ontologies/mathex_onto.thy | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy
index 2a00ee42..507e97d1 100644
--- a/ontologies/mathex_onto.thy
+++ b/ontologies/mathex_onto.thy
@@ -9,6 +9,8 @@ doc_class Question =
 doc_class Response =
   content :: "(string + term) list"
 
+datatype grades = A | B | C  
+  
 doc_class Exercise_part = 
   question :: Question
   response :: Response
@@ -19,4 +21,15 @@ doc_class Exercise=
 doc_class MathExam=
   content :: "(Exercise) list"
 
+section{* Example*}  
+ 
+term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ] "
+  
+text{*
+      @{term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ]"}} are the theorems
+of the equational logic fragment of HOL.
+*}
+
+  
+  
 end
\ No newline at end of file