src/HOL/Metis.thy
 author haftmann Mon Nov 29 13:44:54 2010 +0100 (2010-11-29) changeset 40815 6e2d17cc0d1d parent 39980 f175e482dabe child 41042 8275f52ac991 permissions -rw-r--r--
equivI has replaced equiv.intro
```     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 {*
```
```    34   Metis_Reconstruct.setup
```
```    35   #> Metis_Tactics.setup
```
```    36 *}
```
```    37
```
```    38 hide_const (open) fequal
```
```    39 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
```
```    40
```
```    41 end
```