Commit 4886df18 authored by Heiko Becker's avatar Heiko Becker

Fix cleanup stuff

parent e1c27762
......@@ -2,8 +2,8 @@
Definition of the computation of the absolute error.
used to verify analsysis result in the final theorem of a certificate.
*)
needs "./daisy_lang.hl";;
needs "./interval_arith.hl";;
needs "./Commands.hl";;
needs "./IntervalArith.hl";;
(*
Abbrev define in place since it is used to define abstract operations and has a
......
(*
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
needs "exps.hl";;
needs "Expressions.hl";;
(*
Next define what a program is.
Currently no loops, only conditionals and assignments
......
......@@ -21,7 +21,7 @@
[ Info ] time:
[ Info ] info: 8 ms, rangeError: 81 ms, analysis: 14 ms, frontend: 2547 ms,
*)
needs "./abs_err.hl";;
needs "./AbsoluteError.hl";;
let cst = define `cst:real = (&1657) / (&5)`;;
(* POW IS INFIX IN HOL LIGHT! DUMB IDEA! *)
......
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