Tue, 09 Nov 2010 14:02:14 +0100 | haftmann | slightly changed fun_map_def | changeset | files |
Tue, 09 Nov 2010 14:02:14 +0100 | haftmann | fun_rel_def is no simp rule by default | changeset | files |
Tue, 09 Nov 2010 14:02:13 +0100 | haftmann | more appropriate specification packages; fun_rel_def is no simp rule by default | changeset | files |
Tue, 09 Nov 2010 14:02:13 +0100 | haftmann | type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions | changeset | files |
Tue, 09 Nov 2010 14:02:13 +0100 | haftmann | more appropriate specification packages; fun_rel_def is no simp rule by default | changeset | files |
Tue, 09 Nov 2010 14:02:12 +0100 | haftmann | type annotations in specifications; fun_rel_def is no simp rule by default | changeset | files |