--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -76,13 +76,13 @@
(* counterexample generator *)
-structure Quickcheck_Narrowing_Result = Proof_Data
+structure Counterexample = Proof_Data
(
type T = unit -> term list option
fun init _ () = error " Quickcheck_Narrowing_Result"
)
-val put_counterexample = Quickcheck_Narrowing_Result.put
+val put_counterexample = Counterexample.put
fun compile_generator_expr ctxt t size =
let
@@ -90,8 +90,7 @@
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
val t = dynamic_value_strict
- (Quickcheck_Narrowing_Result.get, Quickcheck_Narrowing_Result.put,
- "Quickcheck_Narrowing.put_counterexample")
+ (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
thy (Option.map o map) (ensure_testable t) []
in
(t, NONE)
--- a/src/HOL/ex/Quickcheck_Narrowing.thy Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing.thy Fri Mar 11 15:21:13 2011 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/ex/LSC_Examples.thy
+(* Title: HOL/ex/Quickcheck_Narrowing_Examples.thy
Author: Lukas Bulwahn
Copyright 2011 TU Muenchen
*)
-header {* Examples for invoking lazysmallcheck (LSC) *}
+header {* Examples for narrowing-based testing *}
-theory LSC_Examples
+theory Quickcheck_Narrowing_Examples
imports "~~/src/HOL/Library/LSC"
begin
--- a/src/HOL/ex/ROOT.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Mar 11 15:21:13 2011 +0100
@@ -77,7 +77,7 @@
];
if getenv "EXEC_GHC" = "" then ()
-else use_thy "LSC_Examples";
+else use_thy "Quickcheck_Narrowing_Examples";
use_thy "SVC_Oracle";
if getenv "SVC_HOME" = "" then ()