src/HOL/Metis.thy
author blanchet
Mon Oct 04 22:45:09 2010 +0200 (2010-10-04)
changeset 39946 78faa9b31202
child 39947 f95834c8bb4d
permissions -rw-r--r--
move Metis into Plain
     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 
    33 setup Metis_Tactics.setup
    34 
    35 end