author  blanchet 
Mon, 11 Oct 2010 18:03:47 +0700  
changeset 39980  f175e482dabe 
parent 39955  cb9cac7eba29 
child 41042  8275f52ac991 
permissions  rwrr 
39946  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" 

39980  32 

33 
setup {* 

34 
Metis_Reconstruct.setup 

35 
#> Metis_Tactics.setup 

36 
*} 

39946  37 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset

38 
hide_const (open) fequal 
39955  39 
hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset

40 

39946  41 
end 