src/HOL/Meson.thy
changeset 39950 f3c4849868b8
parent 39948 317010af8972
child 39953 aa54f347e5e2
     1.1 --- a/src/HOL/Meson.thy	Tue Oct 05 10:30:50 2010 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 10:59:12 2010 +0200
     1.3 @@ -188,21 +188,12 @@
     1.4  
     1.5  section {* Meson package *}
     1.6  
     1.7 -ML {*
     1.8 -structure Meson_Choices = Named_Thms
     1.9 -(
    1.10 -  val name = "meson_choice"
    1.11 -  val description = "choice axioms for MESON's (and Metis's) skolemizer"
    1.12 -)
    1.13 -*}
    1.14 -
    1.15  use "Tools/Meson/meson.ML"
    1.16  use "Tools/Meson/meson_clausify.ML"
    1.17  use "Tools/Meson/meson_tactic.ML"
    1.18  
    1.19  setup {*
    1.20 -  Meson_Choices.setup
    1.21 -  #> Meson.setup
    1.22 +  Meson.setup
    1.23    #> Meson_Tactic.setup
    1.24  *}
    1.25