build

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

Citadelle/ROOT

@@ -121,13 +121,14 @@ session "Citadelle_C_model-dirty" in "src" = "Citadelle_C_shallow-dirty" +
 
 (******************************************************)
 
-session "Max-dirty" in "src" = "HOL-Library" +
+session "Max-dirty" in "src" = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
   options [quick_and_dirty,document=pdf,document_output=document_generated,
            document_variants="document=afp,-annexa,-noexample",
            show_question_marks = false]
   sessions
     OCL
     FOCL
+    Isabelle_Meta_Model
   theories
     "../src/basic_types/UML_UnlimitedNatural"
 

Citadelle/src/compiler/meta/Printer_init.thy

@@ -42,8 +42,8 @@
 section\<open>Initializing the Printer\<close>
 
 theory  Printer_init
-imports "../../compiler_generic/Init"
-        "../../compiler_generic/isabelle_home/src/HOL/Isabelle_Main1"
+imports Isabelle_Meta_Model.Init
+        Isabelle_Meta_Model.Isabelle_Main1
   keywords "lazy_code_printing" "apply_code_printing" "apply_code_printing_reflect"
            :: thy_decl
 begin