diff -r cb1cbae54dbf -r 9c68004b8c9d src/HOL/Metis.thy
--- 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 *}