equal
deleted
inserted
replaced
30 val def_fix_ind = @{thm def_fix_ind}; |
30 val def_fix_ind = @{thm def_fix_ind}; |
31 |
31 |
32 |
32 |
33 fun fixrec_err s = error ("fixrec definition error:\n" ^ s); |
33 fun fixrec_err s = error ("fixrec definition error:\n" ^ s); |
34 fun fixrec_eq_err thy s eq = |
34 fun fixrec_eq_err thy s eq = |
35 fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq)); |
35 fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); |
36 |
36 |
37 (* ->> is taken from holcf_logic.ML *) |
37 (* ->> is taken from holcf_logic.ML *) |
38 (* TODO: fix dependencies so we can import HOLCFLogic here *) |
38 (* TODO: fix dependencies so we can import HOLCFLogic here *) |
39 infixr 6 ->>; |
39 infixr 6 ->>; |
40 fun S ->> T = Type (@{type_name "->"},[S,T]); |
40 fun S ->> T = Type (@{type_name "->"},[S,T]); |