Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
authorlcp
Wed, 03 May 1995 13:35:09 +0200
changeset 1088 fc4fb6e8a636
parent 1087 c1ccf6679a96
child 1089 e679617661bc
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/simpdata.ML	Wed May 03 12:22:17 1995 +0200
+++ b/src/FOL/simpdata.ML	Wed May 03 13:35:09 1995 +0200
@@ -131,9 +131,13 @@
 
 val FOL_ss = IFOL_ss addsimps cla_rews;
 
+(*Used in ZF, perhaps elsewhere?*)
+val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
+  (fn [prem] => [rewtac prem, rtac refl 1]);
+
 (*** case splitting ***)
 
-qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
+qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
 
 local val mktac = mk_case_split_tac meta_iffD
isabelle