src/HOL/Predicate_Compile_Examples/Examples.thy
changeset 52666 391913d17d15
parent 51144 0ede9e2266a8
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 15 20:13:30 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 15 20:36:27 2013 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4                           (s1 @ rhs @ s2) = rsl \<and>
     1.5                           (rule lhs rhs) \<in> fst g }"
     1.6  
     1.7 -definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
     1.8 +definition derivesp ::
     1.9 +  "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
    1.10  where
    1.11    "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
    1.12   
    1.13 @@ -252,7 +253,8 @@
    1.14  where
    1.15    irconst: "eval_var (IrConst i) conf (IntVal i)"
    1.16  | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
    1.17 -| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
    1.18 +| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow>
    1.19 +    eval_var (Add l r) conf (IntVal (vl+vr))"
    1.20  
    1.21  
    1.22  code_pred eval_var .