Commit de0ab718 authored by Heiko Becker's avatar Heiko Becker

Merge branch with HOL Makefile fix and push forward CakeML to latest state to...

Merge branch with HOL Makefile fix and push forward CakeML to latest state to make it compile with current HOL
parent 5e8e8947
......@@ -23,7 +23,7 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib \
cakeml/basis/ioProgLib
cakeml/basis/basis_ffiLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
Subproject commit 4273d509b99f86716a40d18895a091bbd043f24d
Subproject commit c760e35a371970c83a07a154bb67d4b842115a1f
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory;
open ml_translatorTheory ml_translatorLib std_preludeTheory basis;
open gcdTheory
val _ = new_theory "realProg";
val _ = translation_extends "ioProg";
val _ = translation_extends "basisProg";
(* real_of_int *)
......@@ -15,8 +15,7 @@ val real_of_int_def = Define `
val real_of_int_num = store_thm("real_of_int_num[simp]",
``real_of_int (& n) = &n``,
rewrite_tac[real_of_int_def]
\\ Cases_on `&n`
\\ fs []);
\\ CASE_TAC \\ fs []);
val real_of_int_add = store_thm("real_of_int_add[simp]",
``real_of_int (m + n) = real_of_int m + real_of_int n``,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment