equal
deleted
inserted
replaced
8 |
8 |
9 text\<open>these really can't be definitions without losing the abstraction\<close> |
9 text\<open>these really can't be definitions without losing the abstraction\<close> |
10 |
10 |
11 axiomatization |
11 axiomatization |
12 Const :: i and (* Abstract type of constants *) |
12 Const :: i and (* Abstract type of constants *) |
13 c_app :: "[i,i] => i" (* Abstract constructor for fun application*) |
13 c_app :: "[i,i] \<Rightarrow> i" (* Abstract constructor for fun application*) |
14 where |
14 where |
15 constNEE: "c \<in> Const \<Longrightarrow> c \<noteq> 0" and |
15 constNEE: "c \<in> Const \<Longrightarrow> c \<noteq> 0" and |
16 c_appI: "\<lbrakk>c1 \<in> Const; c2 \<in> Const\<rbrakk> \<Longrightarrow> c_app(c1,c2) \<in> Const" |
16 c_appI: "\<lbrakk>c1 \<in> Const; c2 \<in> Const\<rbrakk> \<Longrightarrow> c_app(c1,c2) \<in> Const" |
17 |
17 |
18 |
18 |