equal
deleted
inserted
replaced
9 (absrep_fun_chk flag ctxt (rty, qty) |
9 (absrep_fun_chk flag ctxt (rty, qty) |
10 |> Syntax.string_of_term ctxt |
10 |> Syntax.string_of_term ctxt |
11 |> writeln; |
11 |> writeln; |
12 equiv_relation_chk ctxt (rty, qty) |
12 equiv_relation_chk ctxt (rty, qty) |
13 |> Syntax.string_of_term ctxt |
13 |> Syntax.string_of_term ctxt |
14 |> writeln) |
14 |> writeln; |
|
15 new_equiv_relation_chk ctxt (rty, qty) |
|
16 |> Syntax.string_of_term ctxt |
|
17 |> writeln) |
15 *} |
18 *} |
16 |
19 |
17 definition |
20 definition |
18 erel1 (infixl "\<approx>1" 50) |
21 erel1 (infixl "\<approx>1" 50) |
19 where |
22 where |
79 @{typ "('a fset) bar"}) |
82 @{typ "('a fset) bar"}) |
80 *} |
83 *} |
81 |
84 |
82 ML {* |
85 ML {* |
83 test_funs absF @{context} |
86 test_funs absF @{context} |
|
87 (@{typ "('a list)"}, |
|
88 @{typ "('a fset)"}) |
|
89 *} |
|
90 |
|
91 ML {* |
|
92 test_funs absF @{context} |
84 (@{typ "('a list) list"}, |
93 (@{typ "('a list) list"}, |
85 @{typ "('a fset) fset"}) |
94 @{typ "('a fset) fset"}) |
86 *} |
95 *} |
87 |
96 |
88 ML {* |
97 ML {* |