src/HOL/Metis.thy
author blanchet
Tue Oct 05 11:45:10 2010 +0200 (2010-10-05)
changeset 39953 aa54f347e5e2
parent 39947 f95834c8bb4d
child 39955 cb9cac7eba29
permissions -rw-r--r--
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
     1 (*  Title:      HOL/Metis.thy
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 *)
     6 
     7 header {* Metis Proof Method *}
     8 
     9 theory Metis
    10 imports Meson
    11 uses "~~/src/Tools/Metis/metis.ML"
    12      ("Tools/Metis/metis_translate.ML")
    13      ("Tools/Metis/metis_reconstruct.ML")
    14      ("Tools/Metis/metis_tactics.ML")
    15 begin
    16 
    17 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    18 "fequal X Y \<longleftrightarrow> (X = Y)"
    19 
    20 lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    21 by (simp add: fequal_def)
    22 
    23 lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    24 by (simp add: fequal_def)
    25 
    26 lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    27 by auto
    28 
    29 use "Tools/Metis/metis_translate.ML"
    30 use "Tools/Metis/metis_reconstruct.ML"
    31 use "Tools/Metis/metis_tactics.ML"
    32 setup Metis_Tactics.setup
    33 
    34 hide_const (open) fequal
    35 hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal
    36 
    37 end