Commit 282f5ff0 authored by Heiko Becker's avatar Heiko Becker

Try fixing some issues

parent d02988ff
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory basis;
open ml_translatorTheory ml_translatorLib std_preludeTheory basis RatProgTheory;
open gcdTheory
val _ = new_theory "realProg";
......@@ -88,6 +88,7 @@ val Eval_REAL_LE = Q.prove(
\\ Cases_on `n` \\ fs [real_of_int_def]
\\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rfs [realTheory.REAL_MUL_LNEG,integerTheory.INT_MUL_CALCULATE]
\\ fs[RatProgTheory.pair_le_def]
\\ qpat_x_assum `(_ <= _:int)` mp_tac
\\ fs [integerTheory.INT_NOT_LE])
|> (fn th => MATCH_MP th pair_le_v_thm)
......
open preamble
open simpLib (* realTheory *)realLib RealArith stringTheory
open ml_translatorTheory ml_translatorLib RatProgTheory cfTacticsLib ioProgLib
open ml_translatorTheory ml_translatorLib RatProgTheory cfTacticsLib basisProgTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
ErrorBoundsTheory IntervalArithTheory DaisyTactics IntervalValidationTheory
......@@ -10,7 +10,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
val _ = new_theory "trans";
val _ = translation_extends "realProg";
val _ = translation_extends "RatProg";
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
......
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