[Hol-checkins] SF.net SVN: hol:[7569] HOL/examples/machine-code/hoare-triple/prog_armLib. sml

[<my...@us...>]

Revision: 7569
          http://hol.svn.sourceforge.net/hol/?rev=7569&view=rev
Author:   myreen
Date:     2009-12-16 11:21:56 +0000 (Wed, 16 Dec 2009)

Log Message:
-----------
Bug fixed.

Modified Paths:
--------------
    HOL/examples/machine-code/hoare-triple/prog_armLib.sml

Modified: HOL/examples/machine-code/hoare-triple/prog_armLib.sml
===================================================================
--- HOL/examples/machine-code/hoare-triple/prog_armLib.sml	2009-12-16 11:09:49 UTC (rev 7568)
+++ HOL/examples/machine-code/hoare-triple/prog_armLib.sml	2009-12-16 11:21:56 UTC (rev 7569)
@@ -112,6 +112,10 @@
   val i = foo (free_varsl (concl th :: hyp th)) [] []
   in INST i th end
 
+val SING_SUBSET = prove(
+  ``!x:'a y. {x} SUBSET y = x IN y``,
+  REWRITE_TAC [INSERT_SUBSET,EMPTY_SUBSET]);
+
 fun introduce_aBYTE_MEMORY th = if
   not (can (find_term (can (match_term ``aM1``))) (concl th))
   then th else let
@@ -177,10 +181,6 @@
     val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
     in th end end
 
-val SING_SUBSET = prove(
-  ``!x:'a y. {x} SUBSET y = x IN y``,
-  REWRITE_TAC [INSERT_SUBSET,EMPTY_SUBSET]);
-
 fun introduce_aM th = let
   val index = ref 0
   fun next_var () = (index := (!index)+1; mk_var("w" ^ int_to_string (!index),``:word32``))


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.