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