From 165c3dc0f630e0f23893f1fce7982482e0b52468 Mon Sep 17 00:00:00 2001
From: Brian Mastenbrook <brian@mastenbrook.net>
Date: Sat, 10 Oct 2015 10:02:23 -0500
Subject: [PATCH] Update the documentation to use `#lang rosette/safe`
 consistently

---
 doc/guide/scribble/datatypes/test.rkt        | 4 ++--
 doc/guide/scribble/essentials/poly.rkt       | 4 ++--
 doc/guide/scribble/essentials/queries.rkt    | 4 ++--
 doc/guide/scribble/libs/rosette-lib-test.rkt | 4 ++--
 doc/guide/scribble/reflection/test.rkt       | 2 +-
 doc/guide/scribble/welcome/welcome.scrbl     | 4 ++--
 6 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/doc/guide/scribble/datatypes/test.rkt b/doc/guide/scribble/datatypes/test.rkt
index c81c4f59..ac5afaa7 100644
--- a/doc/guide/scribble/datatypes/test.rkt
+++ b/doc/guide/scribble/datatypes/test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 
 
@@ -33,4 +33,4 @@
 (label (if b (suit 'club) 3))
 
 (define env (solve (assert (suit<? s (suit 'diamond)))))
-(evaluate s env)
\ No newline at end of file
+(evaluate s env)
diff --git a/doc/guide/scribble/essentials/poly.rkt b/doc/guide/scribble/essentials/poly.rkt
index 5ff3c9dc..d8280bd5 100644
--- a/doc/guide/scribble/essentials/poly.rkt
+++ b/doc/guide/scribble/essentials/poly.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 ;(configure [bitwidth 8])
 
@@ -40,4 +40,4 @@
                 (assert (< (abs y) 10))
                 (assert (not (= (poly x) 0)))
                 (assert (= (poly x) (poly y))))))
-env
\ No newline at end of file
+env
diff --git a/doc/guide/scribble/essentials/queries.rkt b/doc/guide/scribble/essentials/queries.rkt
index d6606358..d435e138 100644
--- a/doc/guide/scribble/essentials/queries.rkt
+++ b/doc/guide/scribble/essentials/queries.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette/safe
+#lang rosette/safe
 
 (define (poly x)
   (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
@@ -30,4 +30,4 @@
                               #:guarantee (same-as-poly factored-sketch n))))
 
 (print-forms sol)
-  
\ No newline at end of file
+  
diff --git a/doc/guide/scribble/libs/rosette-lib-test.rkt b/doc/guide/scribble/libs/rosette-lib-test.rkt
index 3f75456f..f61fb9ad 100644
--- a/doc/guide/scribble/libs/rosette-lib-test.rkt
+++ b/doc/guide/scribble/libs/rosette-lib-test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (require rosette/lib/meta/meta)
 
@@ -25,4 +25,4 @@
  (synthesize #:forall (list i)
              #:assume (assert (>= i 0))
              #:guarantee (assert (= (div2mul4 i) (* 4 (quotient i 2))))))
-(print-forms m2)
\ No newline at end of file
+(print-forms m2)
diff --git a/doc/guide/scribble/reflection/test.rkt b/doc/guide/scribble/reflection/test.rkt
index 7594ebe0..33066874 100644
--- a/doc/guide/scribble/reflection/test.rkt
+++ b/doc/guide/scribble/reflection/test.rkt
@@ -1,4 +1,4 @@
-#lang s-exp rosette
+#lang rosette
 
 (define-symbolic b boolean?)
 (define v (vector 1))
diff --git a/doc/guide/scribble/welcome/welcome.scrbl b/doc/guide/scribble/welcome/welcome.scrbl
index 8baecdc5..decc4985 100644
--- a/doc/guide/scribble/welcome/welcome.scrbl
+++ b/doc/guide/scribble/welcome/welcome.scrbl
@@ -66,11 +66,11 @@ The Rosette system ships with two dialects of the Rosette language:
 
 To use the safe dialect, start your programs with the following line:
 
-@racketmod[s-exp rosette/safe]
+@racketmod[rosette/safe]
 
 To use the unsafe dialect, type this line instead:
 
-@racketmod[s-exp rosette]
+@racketmod[rosette]
 
 We strongly recommend that you start with the safe dialect, which includes a core subset of Racket.  The unsafe dialect includes all of Racket, but unless you understand and observe the restrictions on using non-core features, your seemingly correct programs may crash or produce unexpected results.