3173
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
1 |
(* quick_and_dirty := true; *)
|
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
2 |
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
|
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
3 |
"Name_Exec", "Lambda_Exec"];
|
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
4 |
use_thys ["Paper"];
|