# HG changeset patch
# User blanchet
# Date 1399972223 -7200
# Node ID 10d9bd4ea94f7e5f5834b2f42f035e1ae7735bad
# Parent  3d1ead21a0555b6ccd8288dc3da5fd6c576d5fc7
hide more internal names

diff -r 3d1ead21a055 -r 10d9bd4ea94f src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Tue May 13 11:10:22 2014 +0200
+++ b/src/HOL/ATP.thy	Tue May 13 11:10:23 2014 +0200
@@ -16,6 +16,7 @@
 ML_file "Tools/ATP/atp_proof.ML"
 ML_file "Tools/ATP/atp_proof_redirect.ML"
 
+
 subsection {* Higher-order reasoning helpers *}
 
 definition fFalse :: bool where
@@ -39,15 +40,15 @@
 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
 
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
-"fequal x y \<longleftrightarrow> (x = y)"
-
 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fAll P \<longleftrightarrow> All P"
 
 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fEx P \<longleftrightarrow> Ex P"
 
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+"fequal x y \<longleftrightarrow> (x = y)"
+
 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
 unfolding fFalse_def fTrue_def by simp
 
@@ -74,11 +75,6 @@
 "fimplies fTrue fFalse = fFalse"
 unfolding fFalse_def fTrue_def fimplies_def by auto
 
-lemma fequal_table:
-"fequal x x = fTrue"
-"x = y \<or> fequal x y = fFalse"
-unfolding fFalse_def fTrue_def fequal_def by auto
-
 lemma fAll_table:
 "Ex (fComp P) \<or> fAll P = fTrue"
 "All P \<or> fAll P = fFalse"
@@ -89,6 +85,11 @@
 "Ex P \<or> fEx P = fFalse"
 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
 
+lemma fequal_table:
+"fequal x x = fTrue"
+"x = y \<or> fequal x y = fFalse"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
 lemma fNot_law:
 "fNot P \<noteq> P"
 unfolding fNot_def by auto
@@ -114,12 +115,6 @@
 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
 
-lemma fequal_laws:
-"fequal x y = fequal y x"
-"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
-"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
-unfolding fFalse_def fTrue_def fequal_def by auto
-
 lemma fAll_law:
 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
 unfolding fNot_def fComp_def fAll_def fEx_def by auto
@@ -128,6 +123,13 @@
 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
 unfolding fNot_def fComp_def fAll_def fEx_def by auto
 
+lemma fequal_laws:
+"fequal x y = fequal y x"
+"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
+"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
+
 subsection {* Setup *}
 
 ML_file "Tools/ATP/atp_problem_generate.ML"
diff -r 3d1ead21a055 -r 10d9bd4ea94f src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Tue May 13 11:10:22 2014 +0200
+++ b/src/HOL/Metis.thy	Tue May 13 11:10:23 2014 +0200
@@ -14,6 +14,7 @@
 ML_file "~~/src/Tools/Metis/metis.ML"
 declare [[ML_print_depth = 10]]
 
+
 subsection {* Literal selection and lambda-lifting helpers *}
 
 definition select :: "'a \<Rightarrow> 'a" where
@@ -45,12 +46,11 @@
 
 setup {* Metis_Tactic.setup *}
 
-hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
-    lambda
-hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
-    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
-    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
-    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
-    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
+hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
+hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
+  fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
+  fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
+  fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws
+  fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
 
 end