changeset 35431 | 8758fe1fc9f8 |
parent 35417 | 47ee18b6ae32 |
child 36176 | 3fe7e97ccca8 |
--- a/src/HOL/Bali/Basis.thy Wed Mar 03 00:32:14 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Wed Mar 03 00:33:02 2010 +0100 @@ -213,11 +213,6 @@ *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) -translations - "option"<= (type) "Option.option" - "list" <= (type) "List.list" - "sum3" <= (type) "Basis.sum3" - section "quantifiers for option type"