Permalink
Browse files

New version of HOL --> MiniML translator

  • Loading branch information...
myreen committed Feb 27, 2012
1 parent 36e17ba commit 29281450488d77df8c4a3235c17b844c523469a0
@@ -0,0 +1,15 @@
+signature ml_translatorLib =
+sig
+
+ include Abbrev
+
+ (* main functionality *)
+
+ val translate : thm -> thm
+
+ (* wrapper functions *)
+
+ val mlDefine : term quotation -> thm * thm
+ val mltDefine : string -> term quotation -> tactic -> thm * thm
+
+end
Oops, something went wrong.

0 comments on commit 2928145

Please sign in to comment.