diff --git a/LICENSE b/LICENSE index ca847288..998cca27 100644 --- a/LICENSE +++ b/LICENSE @@ -1,7 +1,4 @@ -Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5 - for the OMG Standard. - http://www.brucker.ch/projects/hol-testgen/ - +http://www.brucker.ch/projects/hol-testgen/ This file is part of HOL-TestGen. Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/ROOT b/ROOT index ec287890..b56284f1 100644 --- a/ROOT +++ b/ROOT @@ -1,8 +1,5 @@ (****************************************************************************** - * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5 - * for the OMG Standard. - * http://www.brucker.ch/projects/hol-testgen/ - * + * http://www.brucker.ch/projects/hol-testgen/ * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/Employee_Model/Analysis/Analysis_OCL.thy b/examples/Employee_Model/Analysis/Analysis_OCL.thy index dd173d21..84d6664e 100644 --- a/examples/Employee_Model/Analysis/Analysis_OCL.thy +++ b/examples/Employee_Model/Analysis/Analysis_OCL.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Analysis_OCL.thy --- OCL Contracts and an Example. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/Employee_Model/Analysis/Analysis_UML.thy b/examples/Employee_Model/Analysis/Analysis_UML.thy index e9d5ee94..92be2d71 100644 --- a/examples/Employee_Model/Analysis/Analysis_UML.thy +++ b/examples/Employee_Model/Analysis/Analysis_UML.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Analysis_UML.thy --- OCL Contracts and an Example. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/Employee_Model/Design/Design_OCL.thy b/examples/Employee_Model/Design/Design_OCL.thy index a644ff95..9a03d57b 100644 --- a/examples/Employee_Model/Design/Design_OCL.thy +++ b/examples/Employee_Model/Design/Design_OCL.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Design_OCL.thy --- OCL Contracts and an Example. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/Employee_Model/Design/Design_UML.thy b/examples/Employee_Model/Design/Design_UML.thy index bb317ce4..af993f81 100644 --- a/examples/Employee_Model/Design/Design_UML.thy +++ b/examples/Employee_Model/Design/Design_UML.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Design_UML.thy --- OCL Contracts and an Example. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/archive/Isabelle_Finite_Set.thy b/examples/archive/Isabelle_Finite_Set.thy index 6a458f03..5293fcf5 100644 --- a/examples/archive/Isabelle_Finite_Set.thy +++ b/examples/archive/Isabelle_Finite_Set.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Isabelle_Finite_Set.thy --- Example using the OCL library. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/archive/OCL_core_experiments.thy b/examples/archive/OCL_core_experiments.thy index 9e827592..4765efc1 100644 --- a/examples/archive/OCL_core_experiments.thy +++ b/examples/archive/OCL_core_experiments.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * OCL_core_experiments.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/archive/OCL_lib_Gogolla_challenge.thy b/examples/archive/OCL_lib_Gogolla_challenge.thy index 7bc5a873..4626f4ad 100644 --- a/examples/archive/OCL_lib_Gogolla_challenge.thy +++ b/examples/archive/OCL_lib_Gogolla_challenge.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * OCL_lib_Gogolla_challenge.thy --- Example using the OCL library. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/archive/OCL_lib_Gogolla_challenge_integer.thy b/examples/archive/OCL_lib_Gogolla_challenge_integer.thy index bc6ba93e..36d82a97 100644 --- a/examples/archive/OCL_lib_Gogolla_challenge_integer.thy +++ b/examples/archive/OCL_lib_Gogolla_challenge_integer.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * OCL_lib_Gogolla_challenge_integer.thy --- Example using the OCL library. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/examples/archive/OCL_lib_Gogolla_challenge_naive.thy b/examples/archive/OCL_lib_Gogolla_challenge_naive.thy index df9aa573..ad3ef3d0 100644 --- a/examples/archive/OCL_lib_Gogolla_challenge_naive.thy +++ b/examples/archive/OCL_lib_Gogolla_challenge_naive.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * OCL_lib_Gogolla_challenge_naive.thy --- Example using the OCL library. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Contracts.thy b/src/UML_Contracts.thy index 5df30bae..507d359a 100644 --- a/src/UML_Contracts.thy +++ b/src/UML_Contracts.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Contracts.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Library.thy b/src/UML_Library.thy index 66ff9e69..2e412bb8 100644 --- a/src/UML_Library.thy +++ b/src/UML_Library.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Library.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Logic.thy b/src/UML_Logic.thy index ed2f056c..a8953293 100644 --- a/src/UML_Logic.thy +++ b/src/UML_Logic.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Logic.thy --- Core definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Main.thy b/src/UML_Main.thy index ce380407..6efb8ab4 100644 --- a/src/UML_Main.thy +++ b/src/UML_Main.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Main.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_OCL.thy b/src/UML_OCL.thy index 98cdf4b5..344dcc83 100644 --- a/src/UML_OCL.thy +++ b/src/UML_OCL.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_OCL.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_PropertyProfiles.thy b/src/UML_PropertyProfiles.thy index ecfd0611..6e4059c9 100644 --- a/src/UML_PropertyProfiles.thy +++ b/src/UML_PropertyProfiles.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_PropertyProfiles.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_State.thy b/src/UML_State.thy index 42ae2487..11167907 100644 --- a/src/UML_State.thy +++ b/src/UML_State.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_State.thy --- State Operations and Objects. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Tools.thy b/src/UML_Tools.thy index 8cdf7f47..0b97c15a 100644 --- a/src/UML_Tools.thy +++ b/src/UML_Tools.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Tools.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/UML_Types.thy b/src/UML_Types.thy index ff26b882..117a46b3 100644 --- a/src/UML_Types.thy +++ b/src/UML_Types.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Types.thy --- Types definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_Boolean.thy b/src/basic_types/UML_Boolean.thy index 691ba840..56536ac6 100644 --- a/src/basic_types/UML_Boolean.thy +++ b/src/basic_types/UML_Boolean.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Boolean.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_Integer.thy b/src/basic_types/UML_Integer.thy index f07f481d..d9790c85 100644 --- a/src/basic_types/UML_Integer.thy +++ b/src/basic_types/UML_Integer.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Integer.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_Real.thy b/src/basic_types/UML_Real.thy index 1b0d1359..698312a2 100644 --- a/src/basic_types/UML_Real.thy +++ b/src/basic_types/UML_Real.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Real.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_String.thy b/src/basic_types/UML_String.thy index 8a696d5a..a4c6ce50 100644 --- a/src/basic_types/UML_String.thy +++ b/src/basic_types/UML_String.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_String.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_UnlimitedNatural.thy b/src/basic_types/UML_UnlimitedNatural.thy index c6760a38..608fb44c 100644 --- a/src/basic_types/UML_UnlimitedNatural.thy +++ b/src/basic_types/UML_UnlimitedNatural.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_UnlimitedNatural.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/basic_types/UML_Void.thy b/src/basic_types/UML_Void.thy index 17b4d73b..b6a2f2d7 100644 --- a/src/basic_types/UML_Void.thy +++ b/src/basic_types/UML_Void.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Void.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/collection_types/UML_Bag.thy b/src/collection_types/UML_Bag.thy index 254476ce..abdb6986 100644 --- a/src/collection_types/UML_Bag.thy +++ b/src/collection_types/UML_Bag.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Bag.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/collection_types/UML_Pair.thy b/src/collection_types/UML_Pair.thy index 8ea34f53..e8827d48 100644 --- a/src/collection_types/UML_Pair.thy +++ b/src/collection_types/UML_Pair.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Pair.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/collection_types/UML_Sequence.thy b/src/collection_types/UML_Sequence.thy index 368a31c1..f250c338 100644 --- a/src/collection_types/UML_Sequence.thy +++ b/src/collection_types/UML_Sequence.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Sequence.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/collection_types/UML_Set.thy b/src/collection_types/UML_Set.thy index 8a24c41d..fd7e01b4 100644 --- a/src/collection_types/UML_Set.thy +++ b/src/collection_types/UML_Set.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * UML_Set.thy --- Library definitions. * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Doc.thy b/src/print_syntax/Doc.thy index b5cc8825..fc56d928 100644 --- a/src/print_syntax/Doc.thy +++ b/src/print_syntax/Doc.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Doc.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Gram.thy b/src/print_syntax/Gram.thy index 69963092..b1a40cfd 100644 --- a/src/print_syntax/Gram.thy +++ b/src/print_syntax/Gram.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Gram.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Gram_Generator_dynamic_sequential.thy b/src/print_syntax/Gram_Generator_dynamic_sequential.thy index 1ab2b21d..a6577471 100644 --- a/src/print_syntax/Gram_Generator_dynamic_sequential.thy +++ b/src/print_syntax/Gram_Generator_dynamic_sequential.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Gram_Generator_dynamic_sequential.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Gram_Main.thy b/src/print_syntax/Gram_Main.thy index a54c866d..09cd46e0 100644 --- a/src/print_syntax/Gram_Main.thy +++ b/src/print_syntax/Gram_Main.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Gram_Main.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Gram_Transcendental.thy b/src/print_syntax/Gram_Transcendental.thy index eb995256..c3c43417 100644 --- a/src/print_syntax/Gram_Transcendental.thy +++ b/src/print_syntax/Gram_Transcendental.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Gram_Transcendental.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France diff --git a/src/print_syntax/Gram_UML_Main.thy b/src/print_syntax/Gram_UML_Main.thy index 8cdffc0a..7b255f0b 100644 --- a/src/print_syntax/Gram_UML_Main.thy +++ b/src/print_syntax/Gram_UML_Main.thy @@ -3,7 +3,6 @@ * for the OMG Standard. * http://www.brucker.ch/projects/hol-testgen/ * - * Gram_UML_Main.thy --- * This file is part of HOL-TestGen. * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France