# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID 118cc349de357d0650da7ce415533ec1e080a3a0
# Parent  6babd86a54a4a73a6006ab3c12aff3e2ad8efbce
compile

diff -r 6babd86a54a4 -r 118cc349de35 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 14 11:24:05 2011 +0200
@@ -695,7 +695,7 @@
 
 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
   Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
-  Metis_Examples/BT.thy Metis_Examples/Clausifier.thy \
+  Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
   Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
   Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
   Metis_Examples/set.thy
diff -r 6babd86a54a4 -r 118cc349de35 src/HOL/Metis_Examples/Clausify.thy
--- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Metis_Examples/Clausifier.thy
+(*  Title:      HOL/Metis_Examples/Clausify.thy
     Author:     Jasmin Blanchette, TU Muenchen
 
 Testing Metis's clausifier.
 *)
 
-theory Clausifier
+theory Clausify
 imports Complex_Main
 begin
 
diff -r 6babd86a54a4 -r 118cc349de35 src/HOL/Metis_Examples/ROOT.ML
--- a/src/HOL/Metis_Examples/ROOT.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Metis_Examples/ROOT.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -5,5 +5,5 @@
 Testing Metis and Sledgehammer.
 *)
 
-use_thys ["Abstraction", "BigO", "BT", "Clausifier", "HO_Reas", "Message",
+use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message",
           "Tarski", "TransClosure", "set"];