equal
deleted
inserted
replaced
46 |
46 |
47 |
47 |
48 (** type declarations **) |
48 (** type declarations **) |
49 |
49 |
50 fun HOL_arity (raw_name, args, mx) thy = |
50 fun HOL_arity (raw_name, args, mx) thy = |
51 thy |> AxClass.axiomatize_arity_i |
51 thy |> AxClass.axiomatize_arity |
52 (Sign.full_name thy (Syntax.type_name raw_name mx), |
52 (Sign.full_name thy (Syntax.type_name raw_name mx), |
53 replicate (length args) HOLogic.typeS, HOLogic.typeS); |
53 replicate (length args) HOLogic.typeS, HOLogic.typeS); |
54 |
54 |
55 fun add_typedecls decls thy = |
55 fun add_typedecls decls thy = |
56 if can (Theory.assert_super HOL.thy) thy then |
56 if can (Theory.assert_super HOL.thy) thy then |