src/HOL/Induct/Com.thy
changeset 19736 d8d0f8f51d69
parent 18260 5597cfcecd49
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Induct/Com.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -34,17 +34,14 @@
     1.4  
     1.5  text{* Execution of commands *}
     1.6  consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
     1.7 -syntax "@exec"  :: "((exp*state) * (nat*state)) set =>
     1.8 -                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
     1.9 -
    1.10 -translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
    1.11  
    1.12 -syntax  eval'   :: "[exp*state,nat*state] =>
    1.13 -                    ((exp*state) * (nat*state)) set => bool"
    1.14 -                                           ("_/ -|[_]-> _" [50,0,50] 50)
    1.15 +abbreviation
    1.16 +  exec_rel  ("_/ -[_]-> _" [50,0,50] 50)
    1.17 +  "csig -[eval]-> s == (csig,s) \<in> exec eval"
    1.18  
    1.19 -translations
    1.20 -    "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
    1.21 +abbreviation (input)
    1.22 +  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)
    1.23 +  "esig -|[eval]-> ns == (esig,ns) \<in> eval"
    1.24  
    1.25  text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    1.26  inductive "exec eval"
    1.27 @@ -105,12 +102,12 @@
    1.28  subsection {* Expressions *}
    1.29  
    1.30  text{* Evaluation of arithmetic expressions *}
    1.31 -consts  eval    :: "((exp*state) * (nat*state)) set"
    1.32 -       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
    1.33 +consts
    1.34 +  eval    :: "((exp*state) * (nat*state)) set"
    1.35  
    1.36 -translations
    1.37 -    "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
    1.38 -    "esig -|-> ns"    == "(esig,ns ) \<in> eval"
    1.39 +abbreviation
    1.40 +  eval_rel :: "[exp*state,nat*state] => bool"         (infixl "-|->" 50)
    1.41 +  "esig -|-> ns == (esig, ns) \<in> eval"
    1.42  
    1.43  inductive eval
    1.44    intros