Nominal/Ex/Exec/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Thu, 31 May 2012 12:01:01 +0100
changeset 3181 ca162f0a7957
parent 3173 9876d73adb2b
permissions -rw-r--r--
added to the simplifier nominal_datatype.fresh lemmas
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"];