# HG changeset patch
# User wenzelm
# Date 1203545699 -3600
# Node ID b9fc7ac04c8b17fd71eab30f0b39e3533308df2b
# Parent  2ae572207783e9c67986df2772b9d08d747e44cd
removed ex/NBE.thy;

diff -r 2ae572207783 -r b9fc7ac04c8b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Feb 20 18:28:16 2008 +0100
+++ b/src/HOL/IsaMakefile	Wed Feb 20 23:14:59 2008 +0100
@@ -680,7 +680,7 @@
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
   ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
   ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
-  ex/NatSum.thy ex/NBE.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
+  ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
   ex/Puzzle.thy ex/Quickcheck_Examples.thy \
   ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
   ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \