equal
deleted
inserted
replaced
43 not_equal (infixl \<open>\<noteq>\<close> 50) where |
43 not_equal (infixl \<open>\<noteq>\<close> 50) where |
44 "x \<noteq> y \<equiv> \<not> (x = y)" |
44 "x \<noteq> y \<equiv> \<not> (x = y)" |
45 |
45 |
46 axiomatization where |
46 axiomatization where |
47 |
47 |
48 (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) |
48 (*Structural rules: contraction, thinning, exchange [Søren Heilmann] *) |
49 |
49 |
50 contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and |
50 contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and |
51 contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and |
51 contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and |
52 |
52 |
53 thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and |
53 thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and |