equal
deleted
inserted
replaced
31 for r :: "('a \<times> 'a) set" |
31 for r :: "('a \<times> 'a) set" |
32 where |
32 where |
33 r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" |
33 r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" |
34 | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+" |
34 | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+" |
35 |
35 |
36 declare rtrancl_def [nitpick_def del] |
36 declare rtrancl_def [nitpick_unfold del] |
37 rtranclp_def [nitpick_def del] |
37 rtranclp_def [nitpick_unfold del] |
38 trancl_def [nitpick_def del] |
38 trancl_def [nitpick_unfold del] |
39 tranclp_def [nitpick_def del] |
39 tranclp_def [nitpick_unfold del] |
40 |
40 |
41 notation |
41 notation |
42 rtranclp ("(_^**)" [1000] 1000) and |
42 rtranclp ("(_^**)" [1000] 1000) and |
43 tranclp ("(_^++)" [1000] 1000) |
43 tranclp ("(_^++)" [1000] 1000) |
44 |
44 |