src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
changeset 56927 4044a7d1720f
parent 54703 499f92dc6e45
child 58249 180f1b3508ed
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:37 2014 +0200
@@ -183,7 +183,7 @@
 quickcheck[tester = smart_exhaustive]
 oops
 
-value [code] "prop_regex a_sol"
+value "prop_regex a_sol"
 
 
 end