src/HOL/Unix/Unix.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 20321 b7c0bf788f50
     1.1 --- a/src/HOL/Unix/Unix.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Unix/Unix.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -352,11 +352,9 @@
     1.4  consts
     1.5    transition :: "(file \<times> operation \<times> file) set"
     1.6  
     1.7 -syntax
     1.8 -  "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
     1.9 -  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    1.10 -translations
    1.11 -  "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition"
    1.12 +abbreviation
    1.13 +  transition_rel  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    1.14 +  "root \<midarrow>x\<rightarrow> root' \<equiv> (root, x, root') \<in> transition"
    1.15  
    1.16  inductive transition
    1.17    intros
    1.18 @@ -510,11 +508,9 @@
    1.19  consts
    1.20    transitions :: "(file \<times> operation list \<times> file) set"
    1.21  
    1.22 -syntax
    1.23 -  "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
    1.24 -  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    1.25 -translations
    1.26 -  "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions"
    1.27 +abbreviation
    1.28 +  transitions_rel  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    1.29 +  "root =xs\<Rightarrow> root' \<equiv> (root, xs, root') \<in> transitions"
    1.30  
    1.31  inductive transitions
    1.32    intros