Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
206e6a195296
Commit
1d197423
authored
Nov 11, 2009
by
wenzelm
Browse files
simultaneous use_thys;
parent
b49ff18f68b0
Changes
5
Hide whitespace changes
Inline
Side-by-side
thys/Example-Submission/ROOT.ML
View file @
206e6a19
...
...
@@ -3,12 +3,12 @@ add_path "../Example";
*)
(* to suppress document generation of some theories, use:
no_document use_thy
"ThisTheory
"
;
no_document use_thy
s [
"ThisTheory
1", "ThisTheory2"]
;
*)
(* for normal theory loading, use:
use_thy
"ThatTheory
"
;
use_thy
s [
"ThatTheory
1", "ThatTheory2", "ThatTheory3"]
;
*)
use_thy
"Submission"
;
use_thy
s
[
"Submission"
]
;
thys/FinFun/ROOT.ML
View file @
206e6a19
no_document
use_thy
"Enum"
;
no_document
use_thy
"Infinite_Set"
;
use_thy
"FinFunSet"
;
no_document
use_thys
[
"Enum"
,
"Infinite_Set"
];
use_thys
[
"FinFunSet"
];
thys/Jinja/ROOT-BV.ML
View file @
206e6a19
use_thy
"BV/BVExec"
;
use_thy
"BV/LBVJVM"
;
use_thy
"BV/BVNoTypeError"
;
use_thys
[
"BV/BVExec"
,
"BV/LBVJVM"
,
"BV/BVNoTypeError"
];
no_document
use_thy
"Efficient_Nat"
;
no_document
use_thy
"Executable_Set"
;
use_thy
"BV/BVExample"
;
no_document
use_thys
[
"Efficient_Nat"
,
"Executable_Set"
];
use_thys
[
"BV/BVExample"
];
thys/Jinja/ROOT-J.ML
View file @
206e6a19
goals_limit
:=
1
;
no_document
use_thy
"List_Prefix"
;
no_document
use_thy
"While_Combinator"
;
no_document
use_thys
[
"List_Prefix"
,
"While_Combinator"
,
"Efficient_Nat"
];
use_thy
"J/TypeSafe"
;
use_thy
"J/Annotate"
;
use_thys
[
"J/TypeSafe"
,
"J/Annotate"
,
(*
use_thy "Example";
*)
(*"Example",*)
no_document
use_thy
"Efficient_Nat"
;
use_thy
"J/execute_Bigstep"
;
use_thy
"J/execute_WellType"
;
"J/execute_Bigstep"
,
"J/execute_WellType"
,
use_thy
"JVM/JVMDefensive"
;
use_thy
"JVM/JVMListExample"
;
"JVM/JVMDefensive"
,
"JVM/JVMListExample"
]
;
thys/WorkerWrapper/ROOT.ML
View file @
206e6a19
(*
no_document use_thy "ThisTheory";
use_thy "ThatTheory";
*)
tolerate_legacy_features
:=
false
;
no_document
use_thy
"LList"
;
no_document
use_thy
"Maybe"
;
no_document
use_thy
"Nats"
;
use_thy
"LFPFusion"
;
use_thy
"WorkerWrapper"
;
use_thy
"CounterExample"
;
use_thy
"WorkerWrapperNew"
;
use_thy
"Accumulator"
;
use_thy
"UnboxedNats"
;
use_thy
"Streams"
;
use_thy
"Continuations"
;
no_document
use_thy
"Backtracking"
;
no_document
use_thy
"Nub"
;
no_document
use_thy
"Last"
;
no_document
use_thys
[
"LList"
,
"Maybe"
,
"Nats"
];
use_thys
[
"LFPFusion"
,
"WorkerWrapper"
,
"CounterExample"
,
"WorkerWrapperNew"
,
"Accumulator"
,
"UnboxedNats"
,
"Streams"
,
"Continuations"
,
"Backtracking"
,
"Nub"
,
"Last"
];
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment