equal
deleted
inserted
replaced
56 with main HOL; the theory loader path already includes this directory |
56 with main HOL; the theory loader path already includes this directory |
57 by default; the following existing theories have been moved here: |
57 by default; the following existing theories have been moved here: |
58 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While |
58 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While |
59 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); |
59 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); |
60 |
60 |
61 * added overloaded operations "inverse" and "divide" (infix "/"); |
61 * HOL basics: added overloaded operations "inverse" and "divide" |
|
62 (infix "/"), syntax for generic "abs" operation; |
62 |
63 |
63 * HOL/typedef: simplified package, provide more useful rules (see also |
64 * HOL/typedef: simplified package, provide more useful rules (see also |
64 HOL/subset.thy); |
65 HOL/subset.thy); |
65 |
66 |
66 |
67 |