Fix a proof in iocatProg

CakeML · Dec 16, 2018 · 754f13d · 754f13d
1 parent b96f4c1
commit 754f13d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/examples/iocatProgScript.sml b/examples/iocatProgScript.sml
@@ -1,11 +1,11 @@
 (*
   Faster cat: process 2048 chars at a time.
 *)
+
 open preamble basis
 
 val _ = new_theory "iocatProg"
 
-
 val _ = translation_extends"basisProg";
 
 val st = get_ml_prog_state;
@@ -198,7 +198,7 @@ val cat_spec0 = Q.prove(
      fs[ALOOKUP_inFS_fname_openFileFS_nextFD]) >>
   qmatch_goalsub_abbrev_tac `STDIO fs'` >>
   xlet_auto_spec (SOME (Q.SPECL[`nextFD fs`,`fs'`] close_STDIO_spec))
-  >- xsimpl
+  >- (xsimpl \\ simp[Abbr`fs'`])
   >- (xsimpl >> fs[InvalidFD_exn_def,Abbr`fs'`,up_stdo_def] >>
       simp[validFileFD_def]
       \\ drule (GEN_ALL ALOOKUP_inFS_fname_openFileFS_nextFD)