move sessions to a separate directory

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14189 3260e6d1-4efc-4170-b0a7-36055960796d

Citadelle/ROOT

@@ -122,44 +122,40 @@ session "Citadelle_C_model-dirty" in "src/compiler_citadelle_c/ml" = "Citadelle_
 
 (******************************************************)
 
-session "Max-dirty" in src = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
+session "Max-dirty" = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
   options [quick_and_dirty]
   sessions
     OCL
     FOCL
-    Isabelle_Meta_Model
   theories
-    "../src/basic_types/UML_UnlimitedNatural"
-
-    "../examples/empirical_evaluation/Class_model"
+    "src/basic_types_extra/UML_UnlimitedNatural"
 
-    "../src/compiler/Generator_static"
-    "../src/compiler/meta/Printer_init"
+    "examples/empirical_evaluation/Class_model"
 
-    "../doc/Employee_AnalysisModel_UMLPart_generated"
-    "../doc/Employee_DesignModel_UMLPart_generated"
+    "doc/Employee_AnalysisModel_UMLPart_generated"
+    "doc/Employee_DesignModel_UMLPart_generated"
 
-    "../examples/Bank_Model"
-    "../examples/Bank_Test_Model"
-    "../examples/Clocks_Lib_Model"
-    (*"../examples/Employee_Model/Analysis_deep"*)
-    "../examples/Employee_Model/Analysis_shallow"
-    (*"../examples/Employee_Model/Design_deep"*)
-    "../examples/Employee_Model/Design_shallow"
-    "../examples/Flight_Model"
-    "../examples/AbstractList"
-    "../examples/LinkedList"
-    (*"../examples/ListRefinement"*)
-    "../examples/archive/Flight_Model_compact"
-    "../examples/archive/Simple_Model"
-    "../examples/archive/Toy_deep"
-    "../examples/archive/Toy_shallow"
+    "examples/uml_ocl/Bank_Model"
+    "examples/uml_ocl/Bank_Test_Model"
+    "examples/uml_ocl/Clocks_Lib_Model"
+    (*"examples/Employee_Model/Analysis_generation/Analysis_deep"*)
+    "examples/Employee_Model/Analysis_generation/Analysis_shallow"
+    (*"examples/Employee_Model/Design_generation/Design_deep"*)
+    "examples/Employee_Model/Design_generation/Design_shallow"
+    "examples/uml_ocl/Flight_Model"
+    "examples/uml_ocl/AbstractList"
+    "examples/uml_ocl/LinkedList"
+    (*"examples/uml_ocl/ListRefinement"*)
+    "examples/archive/uml_ocl/Flight_Model_compact"
+    "examples/archive/uml_ocl/Simple_Model"
+    "examples/archive/uml_ocl/Toy_deep"
+    "examples/archive/uml_ocl/Toy_shallow"
 
-    "../src/compiler/Aux_proof"
-    "../src/compiler/Aux_tactic"
-    "../src/compiler/Aux_text"
-    "../src/compiler/Rail"
+    "src/compiler_misc/Aux_proof"
+    "src/compiler_misc/Aux_tactic"
+    "src/compiler_misc/Aux_text"
+    "src/compiler_misc/Rail"
 
-    "../examples/archive/OCL_core_experiments"
-    "../examples/archive/OCL_lib_Gogolla_challenge_naive"
-    "../examples/archive/OCL_lib_Gogolla_challenge_integer"
+    "examples/archive/uml_ocl/OCL_core_experiments"
+    "examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive"
+    "examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_integer"

Citadelle/examples/archive/Toy_deep.thy → Citadelle/examples/archive/uml_ocl/Toy_deep.thy

@@ -379,11 +379,11 @@ subsection\<open>Designing Class Models (V): Inspection of Generated Files\<clos
 text\<open>
 According to options given to the (first) command @{command generation_syntax} above,
 we retrieve the first generated file in the mentioned directory:
-@{file "../../doc/Employee_DesignModel_UMLPart_generated.thy"}.
+@{file "../../../doc/Employee_DesignModel_UMLPart_generated.thy"}.
 
 Because this file still contains meta-commands, we are here executing again
 a new generating step inside this file, the new result becomes saved in
-@{file "../../doc/Employee_DesignModel_UMLPart_generated_generated.thy"}.
+@{file "../../../doc/Employee_DesignModel_UMLPart_generated_generated.thy"}.
 As remark, in this last file, the dependency to @{theory FOCL.Generator_dynamic_sequential} was
 automatically removed because the meta-compiler has detected the absence of meta-commands
 in the generated content.