equal
deleted
inserted
replaced
4 |
4 |
5 theory Transitive_Closure_Table_Ex |
5 theory Transitive_Closure_Table_Ex |
6 imports "~~/src/HOL/Library/Transitive_Closure_Table" |
6 imports "~~/src/HOL/Library/Transitive_Closure_Table" |
7 begin |
7 begin |
8 |
8 |
9 datatype ty = A | B | C |
9 datatype_new ty = A | B | C |
10 |
10 |
11 inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool" |
11 inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool" |
12 where |
12 where |
13 "test A B" |
13 "test A B" |
14 | "test B A" |
14 | "test B A" |