compile
authorblanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42343118cc349de35
parent 42342 6babd86a54a4
child 42344 4a58173ffb99
compile
src/HOL/IsaMakefile
src/HOL/Metis_Examples/Clausify.thy
src/HOL/Metis_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -695,7 +695,7 @@
     1.4  
     1.5  $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
     1.6    Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
     1.7 -  Metis_Examples/BT.thy Metis_Examples/Clausifier.thy \
     1.8 +  Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
     1.9    Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
    1.10    Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
    1.11    Metis_Examples/set.thy
     2.1 --- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
     2.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
     2.3 @@ -1,10 +1,10 @@
     2.4 -(*  Title:      HOL/Metis_Examples/Clausifier.thy
     2.5 +(*  Title:      HOL/Metis_Examples/Clausify.thy
     2.6      Author:     Jasmin Blanchette, TU Muenchen
     2.7  
     2.8  Testing Metis's clausifier.
     2.9  *)
    2.10  
    2.11 -theory Clausifier
    2.12 +theory Clausify
    2.13  imports Complex_Main
    2.14  begin
    2.15  
     3.1 --- a/src/HOL/Metis_Examples/ROOT.ML	Thu Apr 14 11:24:05 2011 +0200
     3.2 +++ b/src/HOL/Metis_Examples/ROOT.ML	Thu Apr 14 11:24:05 2011 +0200
     3.3 @@ -5,5 +5,5 @@
     3.4  Testing Metis and Sledgehammer.
     3.5  *)
     3.6  
     3.7 -use_thys ["Abstraction", "BigO", "BT", "Clausifier", "HO_Reas", "Message",
     3.8 +use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message",
     3.9            "Tarski", "TransClosure", "set"];