Nominal/Ex/Exec/ROOT.ML
author webertj
Tue, 26 Mar 2013 16:41:31 +0100
changeset 3213 a8724924a62e
parent 3173 9876d73adb2b
permissions -rw-r--r--
Manual merge of d121bd2a5a47 from Isabelle/AFP.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3173
9876d73adb2b Executing Lambda Terms
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     1
(* quick_and_dirty := true; *)
9876d73adb2b Executing Lambda Terms
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     2
no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
9876d73adb2b Executing Lambda Terms
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     3
                      "Name_Exec", "Lambda_Exec"];
9876d73adb2b Executing Lambda Terms
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     4
use_thys ["Paper"];