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.
reenabled equality proxy in Metis for higher-order reasoning
authorblanchet
Thu, 12 May 2011 15:29:19 +0200
changeset 42745 b817c6f91a98
parent 42744 59753d5448e0
child 42746 7e227e9de779
reenabled equality proxy in Metis for higher-order reasoning
src/HOL/Tools/Metis/metis_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -532,7 +532,7 @@
   | string_of_mode HO = "HO"
   | string_of_mode FT = "FT"
 
-fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+fun fn_isa_to_met_sublevel "equal" = "c_fequal"
   | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
   | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
   | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
isabelle