equal
deleted
inserted
replaced
12 syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50) |
12 syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50) |
13 |
13 |
14 translations |
14 translations |
15 "x <~~> y" == "(x,y) : perm" |
15 "x <~~> y" == "(x,y) : perm" |
16 |
16 |
17 inductive "perm" |
17 inductive perm |
18 intrs |
18 intrs |
19 Nil "[] <~~> []" |
19 Nil "[] <~~> []" |
20 swap "y#x#l <~~> x#y#l" |
20 swap "y#x#l <~~> x#y#l" |
21 Cons "xs <~~> ys ==> z#xs <~~> z#ys" |
21 Cons "xs <~~> ys ==> z#xs <~~> z#ys" |
22 trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs" |
22 trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs" |