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 * HOLHyperreal: a new target, extending HOLReal with the hyperreals and 

82 Fleuriot's mechanization of analysis; 

83 

84 * HOLReal, HOLHyperreals: improved arithmetic simplification; 
81 
85 
82 *** CTT *** 
86 *** CTT *** 
83 
87 
84 * CTT: xsymbol support for Pi, Sigma, >, : (membership); note that 
88 * CTT: xsymbol support for Pi, Sigma, >, : (membership); note that 
85 "lam" is displayed as TWO lambdasymbols 
89 "lam" is displayed as TWO lambdasymbols 