diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 239b97c..f4045db 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -234,15 +234,16 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
      We call document classes with an \<open>accepts_clause\<close> 
      \<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
      \<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
-           (invariant_decl*) 
+           (invariant_decl?) 
            (accepts_clause rejects_clause?)?\<close>
 \<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
      \<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
 \<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
      Invariants can be specified as predicates over document classes represented as 
      records in HOL. Note that sufficient type information must be provided in order to
-     disambiguate the argument of the \<open>\<lambda>\<close>-expression. 
-     \<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
+     disambiguate the argument of the expression
+     and the \<^boxed_text>\<open>\<sigma>\<close> symbol is reserved to reference the instance of the class itself. 
+     \<^rail>\<open> 'invariant' name '::' '"' term '"' + 'and' \<close>
 \<^item> \<open>accepts_clause\<close>:\<^index>\<open>accepts\_clause@\<open>accepts_clause\<close>\<close>
      \<^rail>\<open> 'accepts' '"' regexpr '"'\<close>
 \<^item> \<open>rejects_clause\<close>:\<^index>\<open>rejects\_clause@\<open>rejects_clause\<close>\<close>
@@ -900,39 +901,43 @@ schemata:
 
 
 section*["sec:advanced"::technical]\<open>Advanced ODL Concepts\<close>
+text\<open>This section will be based on the following example.\<close>
 
-text\<open>For example, assume the following local ontology: 
+subsection*["sec:example"::technical]\<open>Example\<close>
+text\<open>Assume the following local ontology: 
 
-@{boxed_theory_text [display] \<open>
+@{boxed_theory_text [display]\<open>
 doc_class title =
-    short_title :: "string option" <= "None"
-doc_class author = email :: "string" <= "''''"
+  short_title :: "string option" <= "None"
+doc_class author =
+  email :: "string" <= "''''"
 datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
 doc_class abstract =
-    keywordlist :: "string list" <= [] safety_level :: "classification" <= "SIL3"
+  keywordlist :: "string list" <= "[]"
+  safety_level :: "classification" <= "SIL3"
 doc_class text_section =
-    authored_by :: "author set" <= "{}" level :: "int option" <= "None"
+  authored_by :: "author set" <= "{}"
+  level :: "int option" <= "None"
 type_synonym notion = string
 doc_class introduction = text_section +
-    authored_by :: "author set"  <= "UNIV" 
-    uses :: "notion set" 
+  authored_by :: "author set"  <= "UNIV" 
+  uses :: "notion set"
 doc_class claim = introduction +
-    based_on :: "notion list" 
+  based_on :: "notion list" 
 doc_class technical = text_section +
-    formal_results :: "thm list" 
+  formal_results :: "thm list" 
 doc_class "definition" = technical +
-    is_formal :: "bool"
-    property  :: "term list" <= "[]" 
-datatype kind = expert_opinion | argument | proof
+  is_formal :: "bool"
+  property  :: "term list" <= "[]" 
+datatype kind = expert_opinion | argument | "proof"
 doc_class result = technical +
-    evidence :: kind
-    property :: "thm list" <= "[]"
+  evidence :: kind
+  property :: "thm list" <= "[]"
 doc_class example = technical +
-    referring_to :: "(notion + definition) set" <= "{}"
+  referring_to :: "(notion + definition) set" <= "{}"
 doc_class "conclusion" = text_section +
-    establish :: "(claim \<times> result) set"
-\<close>
-}
+  establish :: "(claim \<times> result) set"
+\<close>}
 \<close>
 
 subsection\<open>Meta-types as Types\<close>
@@ -950,20 +955,101 @@ text\<open>
   conventional type-checking that this string represents actually a
   defined entity in the context of the system state
   \<^boxed_theory_text>\<open>\<theta>\<close>.  For example, the \<^boxed_theory_text>\<open>establish\<close>
-  attribute in the previous section is the power of the ODL: here, we model
+  attribute in our example is the power of the ODL: here, we model
   a relation between \<^emph>\<open>claims\<close> and \<^emph>\<open>results\<close> which may be a
   formal, machine-check theorem of type \<^ML_type>\<open>thm\<close> denoted by, for
   example: \<^boxed_theory_text>\<open>property = "[@{thm "system_is_safe"}]"\<close> in a
   system context \<^boxed_theory_text>\<open>\<theta>\<close> where this theorem is
   established. Similarly, attribute values like 
-  \<^boxed_theory_text>\<open>property = "@{term \<open>A \<leftrightarrow> B\<close>}"\<close>
-  require that the HOL-string \<^boxed_theory_text>\<open>A \<leftrightarrow> B\<close> is 
+  \<^boxed_theory_text>\<open>property = "@{term \<open>A \<longleftrightarrow> B\<close>}"\<close>
+  require that the HOL-string \<^boxed_theory_text>\<open>A \<longleftrightarrow> B\<close> is 
   again type-checked and represents indeed a formula in \<open>\<theta>\<close>. Another instance of 
   this process, which we call \<open>second-level type-checking\<close>, are term-constants
   generated from the ontology such as 
   \<^boxed_theory_text>\<open>@{definition <string>}\<close>. 
 \<close>
 
+(*<*)
+declare_reference*["sec:monitors"::technical]
+declare_reference*["sec:low_level_inv"::technical]
+(*>*)
+
+subsection*["sec:class_inv"::technical]\<open>ODL Class Invariants\<close>
+
+
+text\<open>
+  Ontological classes as described so far are too liberal in many situations.
+  There is a first high-level syntax implementation for class invariants.
+  These invariants can be checked when an instance of the class is defined.
+  To enable the checking of the invariants, the \<^boxed_theory_text>\<open>invariants_checking\<close>
+  theory attribute must be set:
+  @{boxed_theory_text [display]\<open>
+  declare[[invariants_checking = true]]\<close>}
+
+  For example, let's define the following two classes:
+  @{boxed_theory_text [display]\<open>
+  doc_class class_inv1 =
+    int1 :: "int"
+    invariant inv1 :: "int1 \<sigma> \<ge> 3"
+
+  doc_class class_inv2 = class_inv1 +
+    int2 :: "int"
+    invariant inv2 :: "int2 \<sigma> < 2"
+  \<close>}
+
+  The \<^boxed_theory_text>\<open>\<sigma>\<close> symbol is reserved and references the future instance class.
+  By relying on the implementation of the Records
+  in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
+  one can reference an attribute of an instance using its selector function.
+  For example, \<^boxed_theory_text>\<open>int1 \<sigma>\<close> denotes the value
+  of the \<^boxed_theory_text>\<open>int1\<close> attribute
+  of the future instance of the class \<^boxed_theory_text>\<open>class_inv1\<close>.
+
+  Now let's define two instances, one of each class:
+
+  @{boxed_theory_text [display]\<open>
+  text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
+  text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
+  \<close>}
+
+  The value of each attribute defined for the instances is checked against their classes invariants.
+  As the class \<^boxed_theory_text>\<open>class_inv2\<close> is a subsclass
+  of the class \<^boxed_theory_text>\<open>class_inv1\<close>, it inherits \<^boxed_theory_text>\<open>class_inv1\<close> invariants.
+  Hence the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
+  when the instance \<^boxed_theory_text>\<open>testinv2\<close> is defined.
+
+  Now let's add some invariants to our example in \<^technical>\<open>sec:example\<close>.
+  For example, one
+  would like to express that any instance of a \<^boxed_theory_text>\<open>result\<close> class finally has
+  a non-empty  property list, if its \<^boxed_theory_text>\<open>kind\<close> is \<^boxed_theory_text>\<open>proof\<close>, or that 
+  the \<^boxed_theory_text>\<open>establish\<close> relation between \<^boxed_theory_text>\<open>claim\<close> and
+  \<^boxed_theory_text>\<open>result\<close> is total.
+  In a high-level syntax, this type of constraints could be expressed, \<^eg>, by:
+  @{boxed_theory_text [display]\<open>
+  doc_class introduction = text_section +
+    authored_by :: "author set"  <= "UNIV" 
+    uses :: "notion set"
+    invariant author_finite :: "finite (authored_by \<sigma>)"
+  doc_class result = technical +
+    evidence :: kind
+    property :: "thm list" <= "[]"
+    invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
+  doc_class example = technical +
+    referring_to :: "(notion + definition) set" <= "{}"
+  doc_class conclusion = text_section +
+    establish :: "(claim \<times> result) set"
+    invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
+                                             \<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
+  \<close>}
+  All specified constraints are already checked in the IDE of \<^dof> while editing.
+  The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the 
+  \<^boxed_theory_text>\<open>authored_by\<close> set.
+  There are still some limitations with this high-level syntax.
+  For now, the high-level syntax does not support  monitors (see \<^technical>\<open>sec:monitors\<close>).
+  For example, one would like to delay a final error message till the
+  closing of a monitor.
+  For this use-case you can use low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).
+\<close>
 
 subsection*["sec:monitors"::technical]\<open>ODL Monitors\<close>
 text\<open>
@@ -1014,49 +1100,33 @@ text\<open>
   smaller than the others. Thus, an introduction is forced to have a
   header delimiting the borders of its representation. Class invariants
   on monitors allow for specifying structural properties on document
-  sections.\<close>
+  sections.
+  For now, the high-level syntax of invariants is not supported for monitors and you must use the
+  the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
 
 
-subsection*["sec:class_inv"::technical]\<open>ODL Class Invariants\<close>
-
+subsection*["sec:low_level_inv"::technical]\<open>ODL Low-level Class Invariants\<close>
 
 text\<open>
-  Ontological classes as described so far are too liberal in many situations. For example, one 
-  would like to express that any instance of a \<^boxed_theory_text>\<open>result\<close> class finally has a 
-  non-empty  property list, if its \<^boxed_theory_text>\<open>kind\<close> is \<^boxed_theory_text>\<open>proof\<close>, or that 
-  the \<^boxed_theory_text>\<open>establish\<close> relation between \<^boxed_theory_text>\<open>claim\<close> and
-  \<^boxed_theory_text>\<open>result\<close> is surjective.
-
-  In a high-level syntax, this type of constraints could be expressed, \<^eg>, by:
-
-@{boxed_theory_text [display]\<open>
-(* 1 *) \<forall> x \<in> result. x@evidence = proo$$f \<leftrightarrow> x@property \<noteq> []
-(* 2 *) \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
-                  \<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
-(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
-\<close>}
-
-  where \<^boxed_theory_text>\<open>result\<close>, \<^boxed_theory_text>\<open>conclusion\<close>, and \<^boxed_theory_text>\<open>introduction\<close> are the set of
-  all possible instances of these document classes.  All specified constraints are already checked
-  in the IDE of \<^dof> while editing; it is however possible to delay a final error message till the 
-  closing of a monitor (see next section). The third constraint enforces that the user sets the 
-  \<^boxed_theory_text>\<open>authored_by\<close> set, otherwise an error will be reported.
-
-  For the moment, there is no high-level syntax for the definition of class invariants. A 
-  formulation, in SML, of the first class-invariant in \<^technical>\<open>sec:class_inv\<close> is straight-forward:
+  If one want to go over the limitations of the actual high-level syntax of the invariant,
+  one can define a function using SML.
+  A formulation, in SML, of the class-invariant \<^boxed_theory_text>\<open>has_property\<close>
+  in \<^technical>\<open>sec:class_inv\<close>, defined in the supposedly \<open>Low_Level_Syntax_Invariants\<close> theory
+  (note the long name of the class),
+  is straight-forward:
 
 \begin{sml}
 fun check_result_inv oid {is_monitor:bool} ctxt =
-  let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
-      val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
+  let val kind = AttributeAccess.compute_attr_access ctxt "evidence" oid <@>{here} <@>{here}
+      val prop = AttributeAccess.compute_attr_access ctxt "property" oid <@>{here} <@>{here}
       val tS = HOLogic.dest_list prop
-  in  case kind_term of
+  in  case kind of
        <@>{term "proof"} => if not(null tS) then true
                           else error("class result invariant violation")
       | _ => false
   end
  val _ = Theory.setup (DOF_core.update_class_invariant
-                                "tiny_cert.result" check_result_inv)
+                                "Low_Level_Syntax_Invariants.result" check_result_inv)
 \end{sml}
 
   The \<^ML>\<open>Theory.setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function 
diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
index 14150b3..eeb5d0e 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
@@ -180,27 +180,7 @@ text\<open>
 
 section\<open>Programming Class Invariants\<close>
 text\<open>
-  For the moment, there is no high-level syntax for the definition of class invariants. A 
-  formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
-
-@{boxed_sml [display]
-\<open>fun check_result_inv oid {is_monitor:bool} ctxt =
-  let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here} 
-      val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here} 
-      val tS = HOLogic.dest_list prop
-  in  case kind_term of
-       <@>{term "proof"} => if not(null tS) then true
-                          else error("class result invariant violation") 
-      | _ => false
-  end
- val _ = Theory.setup (DOF_core.update_class_invariant 
-                                "tiny_cert.result" check_result_inv)\<close>}
-
-  The \<^boxed_sml>\<open>setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function 
-  into the \<^isadof> kernel, which activates any creation or modification of an instance of
-  \<^boxed_theory_text>\<open>result\<close>.  We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding 
-  antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
-  bound to a variable here and can therefore not be statically expanded.
+  See \<^technical>\<open>sec:low_level_inv\<close>.
 \<close>
 
 section\<open>Implementing Monitors\<close>
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 6826442..f163c05 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -63,8 +63,14 @@ val docclassN = "doc_class";
 
 (** name components **)
 
-val makeN = "make";
+val defN = "def"
+val def_suffixN = "_" ^ defN
+val defsN = defN ^ "s"
 val instances_of_suffixN = "_instances"
+val invariant_suffixN = "_inv"
+val invariantN = "\<sigma>"
+val makeN = "make"
+val schemeN = "_scheme"
 
 (* derived from: theory_markup *) 
 fun docref_markup_gen refN def name id pos =
@@ -534,13 +540,13 @@ fun get_object_local oid ctxt  = case get_object_local_opt oid ctxt of
                                       |SOME(bbb) => bbb
 
 fun get_doc_class_global cid thy = 
-    if cid = default_cid then error("default class acces") (* TODO *)
+    if cid = default_cid then error("default class access") (* TODO *)
     else let val t = #docclass_tab(get_data_global thy)
          in  (Symtab.lookup t cid) end
     
 
 fun get_doc_class_local cid ctxt = 
-    if cid = default_cid then error("default class acces") (* TODO *)
+    if cid = default_cid then error("default class access") (* TODO *)
     else let val t = #docclass_tab(get_data ctxt)
          in  (Symtab.lookup t cid) end
 
@@ -799,11 +805,20 @@ val _ =
 val (strict_monitor_checking, strict_monitor_checking_setup) 
      = Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
 
+val (invariants_checking, invariants_checking_setup) 
+     = Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K false);
+
+val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) 
+     = Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
+
+
 end (* struct *)
 
 \<close>
 
-setup\<open>DOF_core.strict_monitor_checking_setup\<close>
+setup\<open>DOF_core.strict_monitor_checking_setup
+      #> DOF_core.invariants_checking_setup
+      #> DOF_core.invariants_checking_with_tactics_setup\<close>
 
 section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
 
@@ -1121,7 +1136,6 @@ fun declare_class_instances_annotation thy doc_class_name =
                     val qual = Long_Name.qualifier long_name
                     val transformer_name = Long_Name.qualify qual
                                 (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind'))
-                    val _ = writeln ("transformer_name: " ^ transformer_name)
                   in
                     DOF_core.update_isa_global (transformer_name,
                     {check=check_identity, elaborate= elaborate_instances_list}) thy end)
@@ -1258,7 +1272,6 @@ fun cid_2_cidType cid_long thy =
              fun fathers cid_long = case Symtab.lookup t cid_long of
                        NONE => let val ctxt = Proof_Context.init_global thy
                                    val tty = Syntax.parse_typ (Proof_Context.init_global thy) cid_long
-                                   val _ = writeln ("XXX"^(Syntax.string_of_typ ctxt tty))
                                in  error("undefined doc class id :"^cid_long)
                                end 
                      | SOME ({inherits_from=NONE, ...}) => [cid_long]
@@ -1413,9 +1426,59 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
                  DOF_core.map_data_global(update_automatons)
       end
 
+fun check_invariants thy oid =
+  let
+    val value = the (DOF_core.get_value_global oid thy)
+    val cid = #cid (the (DOF_core.get_object_global oid thy))
+    fun get_all_invariants cid thy =
+      let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
+      in case DOF_core.get_doc_class_global cid thy of
+             NONE => error("undefined class id for invariants: " ^ cid)
+           | SOME ({inherits_from=NONE, ...}) => invs
+           | SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
+      end
+    val invariants = get_all_invariants cid thy
+    val inv_and_apply_list = 
+      let fun mk_inv_and_apply inv value thy =
+            let val ((s, pos), _ (*term*)) = inv
+                val inv_def = Syntax.read_term_global thy (s ^ invariant_suffixN)
+                val inv_def_typ = Term.type_of value
+            in case inv_def of
+                   Const (s, Type (st, [_ (*ty*), ty'])) =>
+                                        ((s, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value)
+                 | _ => ((s, pos), inv_def $ value)
+            end    
+      in map (fn inv => mk_inv_and_apply inv value thy) invariants
+      end
+    fun check_invariants' ((inv_name, pos), term) =
+      let val ctxt = Proof_Context.init_global thy
+          val evaluated_term = Value_Command.value ctxt term
+                handle ERROR e =>
+                  if (String.isSubstring "Wellsortedness error" e)
+                      andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
+                   then (warning("Invariants checking uses proof tactics");
+                         let val prop_term = HOLogic.mk_Trueprop term
+                             val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
+                             (* Get the make definition (def(1) of the record) *)
+                             val thms' =
+                                  (Proof_Context.get_thms ctxt (Long_Name.append cid defsN)) @ thms
+                             val _ = Goal.prove ctxt [] [] prop_term
+                                                  (K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
+                                     |> Thm.close_derivation \<^here>
+                         (* If Goal.prove does not fail, then the evaluation is considered True,
+                            else an error is triggered by Goal.prove *)
+                         in @{term True} end)
+                   else (error e)
+      in (if evaluated_term = \<^term>\<open>True\<close>
+          then ((inv_name, pos), term)
+          else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
+      end
+    val _ = map check_invariants' inv_and_apply_list 
+  in thy end
 
 fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy = 
-  let val id = serial ();
+  let
+    val id = serial ();
     val _ = Position.report pos (docref_markup true oid id pos);
     (* creates a markup label for this position and reports it to the PIDE framework;
      this label is used as jump-target for point-and-click feature. *)
@@ -1442,7 +1505,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
                             val (value_term', _(*ty*), _) = calc_update_term thy cid_long assns' defaults
                           in value_term' end
     val check_inv =   (DOF_core.get_class_invariant cid_long thy oid is_monitor) 
-                            o Context.Theory 
+                            o Context.Theory
+
   in thy |> DOF_core.define_object_global (oid, {pos      = pos, 
                                                  thy_name = Context.theory_name thy,
                                                  value    = value_term,
@@ -1452,6 +1516,9 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
                                                  vcid     = vcid})
          |> register_oid_cid_in_open_monitors oid pos cid_long
          |> (fn thy => (check_inv thy; thy))
+         |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+                       then check_invariants thy oid
+                       else thy)
   end
 
 
@@ -2134,15 +2201,39 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
 
 fun define_cond binding f_sty   cond_suffix read_cond (ctxt:local_theory) = 
        let val bdg = Binding.suffix_name cond_suffix binding
-           val eq =  mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond ctxt)
+           val eq =  mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond)
            val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
        in def_cmd args true ctxt end
 
 fun define_inv cid_long ((lbl, pos), inv) thy = 
-    let val bdg = (* Binding.suffix_name cid_long *) (Binding.make (lbl,pos))
-        fun inv_term ctxt = Syntax.read_term ctxt inv
-        val inv_ty = (Syntax.read_typ_global thy cid_long) --> HOLogic.boolT
-    in  thy |> Named_Target.theory_map (define_cond bdg inv_ty "_inv" inv_term) end
+    let val bdg = Binding.make (lbl,pos)
+        val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
+        fun update_attribute_type thy class_scheme_ty
+            (Const (s, Type (st,[ty, ty'])) $ t) =
+              let
+                val cid = Long_Name.qualifier s
+              in case DOF_core.get_doc_class_global cid thy of
+                     NONE => Const (s, Type(st,[ty, ty']))
+                             $ (update_attribute_type thy class_scheme_ty t)
+                   | SOME _ => Const(s, Type(st,[class_scheme_ty, ty']))
+                               $ (update_attribute_type thy class_scheme_ty t)
+              end
+          | update_attribute_type thy class_scheme_ty (t $ t') =
+              (update_attribute_type thy class_scheme_ty t)
+              $ (update_attribute_type thy class_scheme_ty t')
+          | update_attribute_type thy class_scheme_ty (Abs(s, ty, t)) =
+              Abs(s, ty, update_attribute_type thy class_scheme_ty t)
+          | update_attribute_type _ class_scheme_ty (Free(s, ty)) = if s = invariantN 
+                                                                     then Free (s, class_scheme_ty)
+                                                                     else Free (s, ty)
+          | update_attribute_type _ _ t = t
+        val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) ("'a " ^ cid_long ^ schemeN)
+        (* Update the type of each attribute update function to match the type of the
+           current class. *)
+        val inv_term' = update_attribute_type thy inv_ty inv_term
+        val eq_inv_ty = inv_ty --> HOLogic.boolT
+        val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term'
+    in  thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end
 
 fun add_doc_class_cmd overloaded (raw_params, binding)
                       raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy
index 68a7c6c..8857b2f 100755
--- a/src/ontologies/Conceptual/Conceptual.thy
+++ b/src/ontologies/Conceptual/Conceptual.thy
@@ -118,9 +118,9 @@ doc_class F  =
                                                  to an association class. It can be used to track
                                                  claims to result - relations, for example.*) 
    b'          :: "(A \<times> C) list"  <= "[]"
-   invariant br :: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
-        and  br':: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
-        and  cr :: "\<lambda>\<sigma>::F. properties \<sigma> \<noteq> []"
+   invariant br :: "r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
+        and  br':: "r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
+        and  cr :: "properties \<sigma> \<noteq> []"
 
 text\<open>The effect of the invariant declaration is to provide intern definitions for validation 
 functions of this invariant. They can be referenced as follows:\<close>
diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy
index 749f381..de669b4 100755
--- a/src/ontologies/scholarly_paper/scholarly_paper.thy
+++ b/src/ontologies/scholarly_paper/scholarly_paper.thy
@@ -137,7 +137,7 @@ doc_class technical = text_section +
    definition_list :: "string list" <=  "[]"
    status          :: status <= "description"
    formal_results  :: "thm list"
-   invariant L1    :: "\<lambda>\<sigma>::technical. the (level \<sigma>) > 0"
+   invariant L1    :: "the (level \<sigma>) > 0"
 
 type_synonym tc = technical (* technical content *)
 
@@ -186,8 +186,8 @@ doc_class math_content = tc +
    short_name    :: string <= "''''"
    status        :: status <= "semiformal"
    mcc           :: "math_content_class" <= "thm" 
-   invariant s1  :: "\<lambda> \<sigma>::math_content. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
-   invariant s2  :: "\<lambda> \<sigma>::math_content. technical.status \<sigma> = semiformal"
+   invariant s1  :: "\<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
+   invariant s2  :: "technical.status \<sigma> = semiformal"
 type_synonym math_tc = math_content
 
 text\<open>The class \<^typ>\<open>math_content\<close> is perhaps more adequaltely described as "math-alike content".
@@ -236,27 +236,28 @@ text\<open>The key class definitions are motivated by the AMS style.\<close>
 doc_class "definition"  = math_content +
    referentiable :: bool <= True
    mcc           :: "math_content_class" <= "defn" 
-   invariant d1  :: "\<lambda> \<sigma>::definition. mcc \<sigma> = defn" (* can not be changed anymore. *)
+   invariant d1  :: "mcc \<sigma> = defn" (* can not be changed anymore. *)
+
 
 doc_class "theorem"     = math_content +
    referentiable :: bool <= True
    mcc           :: "math_content_class" <= "thm" 
-   invariant d2  :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
+    invariant d2  :: "mcc \<sigma> = thm"
 
 doc_class "lemma"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "lem" 
-   invariant d3  :: "\<lambda> \<sigma>::lemma. mcc \<sigma> = lem"
+   invariant d3  :: "mcc \<sigma> = lem"
 
 doc_class "corollary"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "cor" 
-   invariant d4  :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
+    invariant d4  :: "mcc \<sigma> = thm"
 
 doc_class "math_example"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "expl" 
-   invariant d5  :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
+   invariant d5  :: "mcc \<sigma> = expl"
 
 
 subsubsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>
diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy
similarity index 99%
rename from src/tests/Concept_ExampleInvariant.thy
rename to src/tests/Concept_Example_Low_Level_Invariant.thy
index a363f76..c1fa53e 100755
--- a/src/tests/Concept_ExampleInvariant.thy
+++ b/src/tests/Concept_Example_Low_Level_Invariant.thy
@@ -14,7 +14,7 @@
 chapter\<open>Setting and modifying attributes of doc-items\<close>
 
 theory 
-  Concept_ExampleInvariant
+  Concept_Example_Low_Level_Invariant
 imports 
   "Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
diff --git a/src/tests/High_Level_Syntax_Invariants.thy b/src/tests/High_Level_Syntax_Invariants.thy
new file mode 100644
index 0000000..805cc59
--- /dev/null
+++ b/src/tests/High_Level_Syntax_Invariants.thy
@@ -0,0 +1,114 @@
+chapter\<open>High level syntax Invariants\<close>
+
+theory High_Level_Syntax_Invariants
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+text\<open>
+  Ontological classes as described so far are too liberal in many situations.
+  There is a first high-level syntax implementation for class invariants.
+  These invariants can be checked when an instance of the class is defined.
+  To enable the checking of the invariants, the \<open>invariants_checking\<close>
+  theory attribute must be set:\<close>
+
+
+declare[[invariants_checking = true]]
+
+text\<open>For example, let's define the following two classes:\<close>
+
+doc_class class_inv1 =
+  int1 :: "int"
+  invariant inv1 :: "int1 \<sigma> \<ge> 3"
+
+doc_class class_inv2 = class_inv1 +
+  int2 :: "int"
+  invariant inv2 :: "int2 \<sigma> < 2"
+
+text\<open>The  symbol \<^term>\<open>\<sigma>\<close> is reserved and references the future instance class.
+  By relying on the implementation of the Records
+  in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
+  one can reference an attribute of an instance using its selector function.
+  For example, \<^term>\<open>int1 \<sigma>\<close> denotes the value
+  of the \<^term>\<open>int1\<close> attribute
+  of the future instance of the class @{doc_class class_inv1}.
+  Now let's define two instances, one of each class:\<close>
+
+text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
+text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
+
+text\<open>
+  The value of each attribute defined for the instances is checked against their classes invariants.
+  As the class @{doc_class class_inv2} is a subsclass of the class @{doc_class class_inv1},
+  it inherits @{doc_class class_inv1} invariants.
+  Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
+
+text\<open>Now assume the following ontology:\<close>
+
+doc_class title =
+  short_title :: "string option" <= "None"
+
+doc_class author =
+  email :: "string" <= "''''"
+
+datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
+
+doc_class abstract =
+  keywordlist :: "string list" <= "[]"
+  safety_level :: "classification" <= "SIL3"
+
+doc_class text_section =
+  authored_by :: "author set" <= "{}"
+  level :: "int option" <= "None"
+
+type_synonym notion = string
+
+doc_class introduction = text_section +
+  authored_by :: "author set"  <= "UNIV" 
+  uses :: "notion set"
+  invariant author_finite :: "finite (authored_by \<sigma>)"
+
+doc_class claim = introduction +
+  based_on :: "notion list"
+
+doc_class technical = text_section +
+  formal_results :: "thm list" 
+
+doc_class "definition" = technical +
+  is_formal :: "bool"
+  property  :: "term list" <= "[]" 
+
+datatype kind = expert_opinion | argument | "proof"
+
+doc_class result = technical +
+  evidence :: kind
+  property :: "thm list" <= "[]"
+  invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
+doc_class example = technical +
+  referring_to :: "(notion + definition) set" <= "{}"
+
+doc_class conclusion = text_section +
+  establish :: "(claim \<times> result) set"
+  invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
+                                            \<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
+
+text\<open>Next we define some instances (docitems): \<close>
+text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
+
+text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
+text*[resultArgument::result, evidence = "argument"]\<open>\<close>
+
+text\<open>The invariants \<open>author_finite\<close> and \<open>total_rel\<close> can not be checked directly
+  and need a little help.
+  We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
+  It will enable a basic tactic, using unfold and auto:\<close>
+
+declare[[invariants_checking_with_tactics = true]]
+
+text*[introductionTest::introduction, authored_by = "{@{author \<open>church\<close>}}"]\<open>\<close>
+
+text*[claimNotion::claim, authored_by = "{@{author \<open>church\<close>}}", based_on= "[\<open>Notion1\<close>, \<open>Notion2\<close>]"]\<open>\<close>
+
+text*[conclusionProof::conclusion,
+      establish = "{(@{claim \<open>claimNotion\<close>}, @{result \<open>resultProof\<close>})}"]\<open>\<close>
+
+end
diff --git a/src/tests/Ontology_Matching_Example.thy b/src/tests/Ontology_Matching_Example.thy
new file mode 100644
index 0000000..d374e7c
--- /dev/null
+++ b/src/tests/Ontology_Matching_Example.thy
@@ -0,0 +1,52 @@
+chapter\<open>Ontologys Mathing\<close>
+
+theory Ontology_Matching_Example
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+text\<open>Using HOL, we can define a mapping between two ontologies.
+  It is called ontology matching or ontology alignment.
+  Here is an example which show how to map two classes.
+  HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
+
+type_synonym UTF8 = string
+
+definition utf8_to_string
+  where "utf8_to_string x = x"
+
+
+doc_class A =
+  first_name :: UTF8
+  last_name :: UTF8
+  age :: nat
+  married_to :: "string option"
+  invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
+doc_class B =
+  name :: string 
+  adult :: bool
+  is_married :: bool
+  invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
+
+text\<open>We define the mapping between the two classes,
+  i.e. how to transform the class @{doc_class A} in to the class @{doc_class B}:\<close>
+
+definition A_to_B_morphism
+  where "A_to_B_morphism X =
+        \<lparr> tag_attribute = A.tag_attribute X
+          , name = utf8_to_string (first_name X) @ '' ''  @ utf8_to_string (last_name X)
+          , adult = (age X \<ge> 18)
+          , is_married = (married_to X \<noteq> None) \<rparr>" 
+
+text\<open>Now we check that the invariant is preserved through the morphism:\<close>
+
+lemma inv_a_preserved :
+  "a_inv X \<Longrightarrow> b_inv (A_to_B_morphism X)"
+  unfolding a_inv_def b_inv_def A_to_B_morphism_def
+  by auto
+
+lemma A_morphism_B_total :
+  "A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
+  using inv_a_preserved
+  by auto
+
+end
diff --git a/src/tests/ROOT b/src/tests/ROOT
index 406d6fb..4ef831b 100755
--- a/src/tests/ROOT
+++ b/src/tests/ROOT
@@ -2,8 +2,10 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
   options [document = false]
   theories
     "AssnsLemmaThmEtc" 
-    "Concept_ExampleInvariant"
+    "Concept_Example_Low_Level_Invariant"
     "Concept_Example"
     "TermAntiquotations"
     "Attributes"
     "Evaluation"
+    "High_Level_Syntax_Invariants"
+    "Ontology_Matching_Example"