src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
changeset 52666 391913d17d15
parent 45451 74515e8e6046
child 54703 499f92dc6e45
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Mon Jul 15 20:13:30 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Mon Jul 15 20:36:27 2013 +0200
     1.3 @@ -85,7 +85,8 @@
     1.4   
     1.5  fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
     1.6  where
     1.7 -  "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
     1.8 +  "prop_regex (n, (k, (p, (q, s)))) =
     1.9 +    ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
    1.10  
    1.11  
    1.12  
    1.13 @@ -97,7 +98,10 @@
    1.14  oops
    1.15  
    1.16  
    1.17 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
    1.18 +setup {*
    1.19 +  Context.theory_map
    1.20 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    1.21 +*}
    1.22  
    1.23  setup {* Code_Prolog.map_code_options (K 
    1.24    {ensure_groundness = true,