equal
deleted
inserted
replaced
76 operator; |
76 operator; |
77 |
77 |
78 * HOL/typedef: simplified package, provide more useful rules (see also |
78 * HOL/typedef: simplified package, provide more useful rules (see also |
79 HOL/subset.thy); |
79 HOL/subset.thy); |
80 |
80 |
|
81 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and |
|
82 Fleuriot's mechanization of analysis; |
|
83 |
|
84 * HOL-Real, HOL-Hyperreals: improved arithmetic simplification; |
81 |
85 |
82 *** CTT *** |
86 *** CTT *** |
83 |
87 |
84 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that |
88 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that |
85 "lam" is displayed as TWO lambda-symbols |
89 "lam" is displayed as TWO lambda-symbols |