Commit 23cf55c1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix regression test for new infrastructure

parent cfab86f5
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra ../../hol4/cakeml/misc
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_AdditionSimple";
......
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_Doppler";
......
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_Himmilbeau";
......
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