# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 398fff2c6b8f21134724964e73511a6ba2884b40
# Parent  04cae06f0b99111c14d4a5b9acca90481db5af3a
use ! for mildly unsound and !! for very unsound encodings

diff -r 04cae06f0b99 -r 398fff2c6b8f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:25 2011 +0200
@@ -238,9 +238,9 @@
       (case try (unprefix "mono_") type_sys of
          SOME s => (true, s)
        | NONE => (false, type_sys))
-      ||> (fn s => case try (unsuffix " **") s of
+      ||> (fn s => case try (unsuffix " !!") s of
                      SOME s => (Unsound, s)
-                   | NONE => case try (unsuffix " *") s of
+                   | NONE => case try (unsuffix " !") s of
                                SOME s => (Half_Sound, s)
                              | NONE => (Sound, s))
       |> (fn (mono, (level, core)) =>
@@ -350,7 +350,9 @@
                   end))
 
 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number)
+val parse_value =
+  Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "!!"
+                || Parse.$$$ "!")
 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =