startpunkt

examples/CENELEC_50128/mini_odo/mini_odo.thy

@@ -556,7 +556,7 @@ result communication times... \<close>
   
 text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command
 that governs the external test-execution via, eg., a makefile or specific calls
-to a test-environment or test-engine \<close>
+to a test-environment or test-engine. \<close>
 
 
 text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared 

src/ontologies/math_exam/Nmath_exam.thy

@@ -116,19 +116,21 @@ exercise - (header ~ context_description ~ task list)
 *)
 
 (*
-tasks & subtask
+tasks  > subtask
 
 answer > subanswer
 
 answer_element
  - text
+ - program-text ? ? ? 
  - checkbox
  - radiobutton
  - equational derivation
  - proof derivation
 
 solution > subsolution
- - test
+ - text
+ - program-text
  - checkbox
  - radiobutton
  - equational derivation
@@ -143,6 +145,7 @@ Invarianten:
 
 2 : invariants over markings and grades
 
+3 : distribution constraints: subtask should have more than 25 % of overall grade 
 
 *)