From b035996d36123b977d7dd5c7e5c71ae25f72be30 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 19 Apr 2019 16:16:54 +0200
Subject: [PATCH] petitesse

---
 ontologies/CENELEC_50128.thy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy
index e63ca22..8ade295 100644
--- a/ontologies/CENELEC_50128.thy
+++ b/ontologies/CENELEC_50128.thy
@@ -734,5 +734,10 @@ Syntax.read_typ  @{context} "hypothesis" handle  _ => dummyT;
 Proof_Context.init_global;
 \<close>
 
+text\<open> 
+ @{theory_text [display] \<open>definition a\<^sub>E \<equiv> True
+                          lemma XXX : "True = False " by auto\<close>} 
+\<close>
+
 end      
   
\ No newline at end of file