src/HOL/Meson.thy
changeset 39948 317010af8972
parent 39947 f95834c8bb4d
child 39950 f3c4849868b8
     1.1 --- a/src/HOL/Meson.thy	Mon Oct 04 22:51:53 2010 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 10:28:11 2010 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  imports Datatype
     1.5  uses ("Tools/Meson/meson.ML")
     1.6       ("Tools/Meson/meson_clausify.ML")
     1.7 +     ("Tools/Meson/meson_tactic.ML")
     1.8  begin
     1.9  
    1.10  section {* Negation Normal Form *}
    1.11 @@ -197,11 +198,12 @@
    1.12  
    1.13  use "Tools/Meson/meson.ML"
    1.14  use "Tools/Meson/meson_clausify.ML"
    1.15 +use "Tools/Meson/meson_tactic.ML"
    1.16  
    1.17  setup {*
    1.18    Meson_Choices.setup
    1.19    #> Meson.setup
    1.20 -  #> Meson_Clausify.setup
    1.21 +  #> Meson_Tactic.setup
    1.22  *}
    1.23  
    1.24  end