equal
deleted
inserted
replaced
44 * new theory section 'setup'; |
44 * new theory section 'setup'; |
45 |
45 |
46 |
46 |
47 *** HOL *** |
47 *** HOL *** |
48 |
48 |
|
49 * HOL/Real: a construction of the reals using Dedekind cuts |
|
50 |
49 * HOL/record: now includes concrete syntax for record terms (still |
51 * HOL/record: now includes concrete syntax for record terms (still |
50 lacks important theorems, like surjective pairing and split); |
52 lacks important theorems, like surjective pairing and split); |
51 |
53 |
52 * simplification procedure unit_eq_proc rewrites (?x::unit) = (); this |
54 * simplification procedure unit_eq_proc rewrites (?x::unit) = (); this |
53 is made part of the default simpset of Prod.thy, which COULD MAKE |
55 is made part of the default simpset of Prod.thy, which COULD MAKE |