[Hol-checkins] SF.net SVN: hol:[6051] HOL/examples

[<sl...@us...>]

Revision: 6051
          http://hol.svn.sourceforge.net/hol/?rev=6051&view=rev
Author:   slind
Date:     2008-07-20 19:25:25 +0000 (Sun, 20 Jul 2008)

Log Message:
-----------
Laggard mods for simpset pp'ing.

Modified Paths:
--------------
    HOL/examples/lambda/basics/basic_swapScript.sml
    HOL/examples/lambda/basics/binderLib.sml
    HOL/examples/lambda/basics/nomsetScript.sml
    HOL/examples/lambda/sttScript.sml
    HOL/examples/mc-logic/helperLib.sml

Modified: HOL/examples/lambda/basics/basic_swapScript.sml
===================================================================
--- HOL/examples/lambda/basics/basic_swapScript.sml	2008-07-20 09:21:14 UTC (rev 6050)
+++ HOL/examples/lambda/basics/basic_swapScript.sml	2008-07-20 19:25:25 UTC (rev 6051)
@@ -7,7 +7,7 @@
 val _ = new_theory "basic_swap";
 
 fun Store_Thm(s, t, tac) = (store_thm(s,t,tac) before
-                            BasicProvers.export_rewrites [s])
+                            export_rewrites [s])
 
 (* ----------------------------------------------------------------------
     swapping over strings

Modified: HOL/examples/lambda/basics/binderLib.sml
===================================================================
--- HOL/examples/lambda/basics/binderLib.sml	2008-07-20 09:21:14 UTC (rev 6050)
+++ HOL/examples/lambda/basics/binderLib.sml	2008-07-20 19:25:25 UTC (rev 6051)
@@ -358,7 +358,7 @@
     val interesting_bit = CONJUNCT2 f_def
   in
     save_thm(fstr^"_swap_invariant", interesting_bit) before
-    export_rewrites [fstr^"_swap_invariant"]
+    export_rewrites (current_theory()) [fstr^"_swap_invariant"]
   end
 in
   (f_thm, f_invariants)

Modified: HOL/examples/lambda/basics/nomsetScript.sml
===================================================================
--- HOL/examples/lambda/basics/nomsetScript.sml	2008-07-20 09:21:14 UTC (rev 6050)
+++ HOL/examples/lambda/basics/nomsetScript.sml	2008-07-20 19:25:25 UTC (rev 6051)
@@ -11,7 +11,7 @@
 val _ = new_theory "nomset";
 
 fun Store_Thm(s, t, tac) = (store_thm(s,t,tac) before
-                            BasicProvers.export_rewrites [s])
+                            export_rewrites [s])
 
 (* permutations are represented as lists of pairs of strings.  These
    can be lifted to bijections on strings that only move finitely many

Modified: HOL/examples/lambda/sttScript.sml
===================================================================
--- HOL/examples/lambda/sttScript.sml	2008-07-20 09:21:14 UTC (rev 6050)
+++ HOL/examples/lambda/sttScript.sml	2008-07-20 19:25:25 UTC (rev 6051)
@@ -14,7 +14,7 @@
 open HolKernel boolLib Parse bossLib
 open binderLib metisLib termTheory;
 
-val export_rewrites = BasicProver.export_rewrites "stt";
+val export_rewrites = BasicProvers.export_rewrites "stt";
 
 val _ = new_theory "stt";
 

Modified: HOL/examples/mc-logic/helperLib.sml
===================================================================
--- HOL/examples/mc-logic/helperLib.sml	2008-07-20 09:21:14 UTC (rev 6050)
+++ HOL/examples/mc-logic/helperLib.sml	2008-07-20 19:25:25 UTC (rev 6051)
@@ -111,7 +111,8 @@
 
 (* simpsets *)
 
-fun conv2ssfrag name conv pattern = simpLib.SSFRAG{ ac = [], congs = [],
+fun conv2ssfrag name conv pattern = simpLib.SSFRAG{name=NONE,
+  ac = [], congs = [],
   convs = [{ name  = name, conv = K (K conv), key = SOME([], pattern), trace = 10 }],
   dprocs = [], filter = NONE, rewrs = []};
 


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