changeset 59557 | ebd8ecacfba6 |
parent 59546 | 3850a2d20f19 |
child 59667 | 651ea265d568 |
--- a/src/HOL/Fields.thy Wed Feb 18 22:46:48 2015 +0100 +++ b/src/HOL/Fields.thy Thu Feb 19 11:53:36 2015 +0100 @@ -1204,7 +1204,9 @@ end +hide_fact (open) field_inverse field_divide_inverse field_inverse_zero + code_identifier code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith - + end