--- a/src/HOL/Metis.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis.thy Wed Dec 15 11:26:28 2010 +0100
@@ -15,17 +15,26 @@
("Tools/try.ML")
begin
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<longleftrightarrow> (X = Y)"
+definition fFalse :: bool where [no_atp]:
+"fFalse \<longleftrightarrow> False"
-lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
-by (simp add: fequal_def)
+definition fTrue :: bool where [no_atp]:
+"fTrue \<longleftrightarrow> True"
+
+definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
+"fNot P \<longleftrightarrow> \<not> P"
-lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
-by (simp add: fequal_def)
+definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fconj P Q \<longleftrightarrow> P \<and> Q"
+
+definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fdisj P Q \<longleftrightarrow> P \<or> Q"
-lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
-by auto
+definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal x y \<longleftrightarrow> (x = y)"
use "Tools/Metis/metis_translate.ML"
use "Tools/Metis/metis_reconstruct.ML"
@@ -36,8 +45,9 @@
#> Metis_Tactics.setup
*}
-hide_const (open) fequal
-hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
+hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
+hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
+ fequal_def
subsection {* Try *}