Skip to content
Snippets Groups Projects
Commit 3e7c41bc authored by Frédéric Tuong's avatar Frédéric Tuong
Browse files

move sessions to a separate directory 

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14180 3260e6d1-4efc-4170-b0a7-36055960796d
parent ad38a5b3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 22 additions and 22 deletions
Citadelle/ROOT
+ 1
− 1
View file @ 3e7c41bc
......@@ -46,7 +46,7 @@ session OCL in src = HOL +
document_variants="annex-a=annexa,-theory,-afp,-noexample,-proof,-ML:document=afp,-annexa,-noexample:outline=-annexa,-noexample,afp,/proof,/ML",
show_question_marks = false]
theories
"../src/UML_Main"
"../src/uml_main/UML_Main"
"../examples/Employee_Model/Analysis/Analysis_OCL"
"../examples/Employee_Model/Design/Design_OCL"
document_files
......
Citadelle/examples/Employee_Model/Analysis/Analysis_UML.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -51,7 +51,7 @@ chapter{* Example: The Employee Analysis Model *} (* UML part *)
theory
Analysis_UML
imports
"../../../src/UML_Main"
"../../../src/uml_main/UML_Main"
begin
text {* \label{ex:employee-analysis:uml} *}
......
Citadelle/examples/Employee_Model/Design/Design_UML.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -51,7 +51,7 @@ chapter{* Example: The Employee Design Model *} (* UML part *)
theory
Design_UML
imports
"../../../src/UML_Main"
"../../../src/uml_main/UML_Main"
begin
text {* \label{ex:employee-design:uml} *}
......
Citadelle/examples/archive/Toy_deep.thy
+ 2
− 2
View file @ 3e7c41bc
......@@ -71,7 +71,7 @@ to see the differences of imported theories, and which ones to manually import
generation_syntax [ (*deep
(generation_semantics [ design (*, oid_start 10*) ])
(THEORY Toy_generated)
(IMPORTS ["../src/UML_Main", "../src/compiler/Static"]
(IMPORTS ["../src/uml_main/UML_Main", "../src/compiler/Static"]
"../src/compiler/Generator_dynamic_sequential")
SECTION
(*SORRY*) (*no_dirty*)
......@@ -89,7 +89,7 @@ generation_syntax
[ deep
(generation_semantics [ design ])
(THEORY Design_generated)
(IMPORTS ["../src/UML_Main", "../src/compiler/Static"]
(IMPORTS ["../src/uml_main/UML_Main", "../src/compiler/Static"]
"../src/compiler/Generator_dynamic_sequential")
SECTION
(*SORRY*) (*no_dirty*)
......
Citadelle/examples/empirical_evaluation/Class_model.thy
+ 2
− 2
View file @ 3e7c41bc
......@@ -86,14 +86,14 @@ definition \<open>print_abr sprintf_int write_file =
, \<open> (generation_semantics [ analysis (*, oid_start 10*) ])\<close>
, \<open> skip_export\<close>
, S.flatten [\<open> (THEORY \<close>, tree_name, \<open>_generated\<close>, \<open>_\<close>, comp, \<open>)\<close>]
, S.flatten [\<open> (IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]\<close>]
, S.flatten [\<open> (IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]\<close>]
, S.flatten [\<open> "../../../src/compiler/Generator_dynamic_sequential")\<close>]
, \<open> SECTION\<close>
, S.flatten [\<open> [ in \<close>, comp, \<open> \<close>, comp2, \<open> ]\<close>]
, S.flatten [\<open> (output_directory "./doc") ]\<close>] ]
, S_flatten_n [ \<open>generation_syntax deep flush_all\<close> ])
, ( (\<open>shallow\<close>, [(\<open>\<close>, \<open>\<close>)])
, S.flatten [ \<open>"../../src/UML_Main"\<close>, \<open> \<close>
, S.flatten [ \<open>"../../src/uml_main/UML_Main"\<close>, \<open> \<close>
, \<open>"../../src/compiler/Static"\<close> ]
, \<lambda>_ _. S_flatten_n [ \<open>generation_syntax [ shallow (generation_semantics [ analysis ]) ]\<close> ]
, \<open>End!\<close>) ]))\<close>
......
Citadelle/examples/empirical_evaluation/Tree_01_00_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_00_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_00_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_00_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_00_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
......
Citadelle/examples/empirical_evaluation/Tree_01_01_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_01_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_01_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_01_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_01_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_02_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_02_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_02_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_02_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_02_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_03_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_03_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_03_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_03_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_03_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_04_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_04_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_04_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_04_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_04_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_05_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_05_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_05_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_05_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_05_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_06_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_06_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
Citadelle/examples/empirical_evaluation/Tree_01_06_shallow.thy
+ 1
− 1
View file @ 3e7c41bc
theory Tree_01_06_shallow imports "../../src/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
theory Tree_01_06_shallow imports "../../src/uml_main/UML_Main" "../../src/compiler/Static" "../../src/compiler/Generator_dynamic_sequential" begin
generation_syntax [ shallow (generation_semantics [ analysis ]) ]
Class Aazz End
......
Citadelle/examples/empirical_evaluation/Tree_01_07_deep_self.thy
+ 1
− 1
View file @ 3e7c41bc
......@@ -3,7 +3,7 @@ generation_syntax [ deep
(generation_semantics [ analysis (*, oid_start 10*) ])
skip_export
(THEORY Tree_01_07_generated_self)
(IMPORTS ["../../../src/UML_Main", "../../../src/compiler/Static"]
(IMPORTS ["../../../src/uml_main/UML_Main", "../../../src/compiler/Static"]
"../../../src/compiler/Generator_dynamic_sequential")
SECTION
[ in self ]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment