equal
deleted
inserted
replaced
9 "~~/src/HOL/Library/FuncSet", |
9 "~~/src/HOL/Library/FuncSet", |
10 "Eval_Examples", |
10 "Eval_Examples", |
11 "Normalization_by_Evaluation", |
11 "Normalization_by_Evaluation", |
12 "Hebrew", |
12 "Hebrew", |
13 "Chinese", |
13 "Chinese", |
14 "Serbian" |
14 "Serbian", |
|
15 "~~/src/HOL/Library/FinFun" |
15 ]; |
16 ]; |
16 |
17 |
17 use_thys [ |
18 use_thys [ |
18 "Iff_Oracle", |
19 "Iff_Oracle", |
19 "Coercion_Examples", |
20 "Coercion_Examples", |
68 "Quicksort", |
69 "Quicksort", |
69 "Birthday_Paradox", |
70 "Birthday_Paradox", |
70 "List_to_Set_Comprehension_Examples", |
71 "List_to_Set_Comprehension_Examples", |
71 "Seq", |
72 "Seq", |
72 "Simproc_Tests", |
73 "Simproc_Tests", |
73 "Executable_Relation" |
74 "Executable_Relation", |
|
75 "FinFunPred" |
74 ]; |
76 ]; |
75 |
77 |
76 use_thy "SVC_Oracle"; |
78 use_thy "SVC_Oracle"; |
77 if getenv "SVC_HOME" = "" then () |
79 if getenv "SVC_HOME" = "" then () |
78 else use_thy "svc_test"; |
80 else use_thy "svc_test"; |