src/HOL/Bali/Basis.thy
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"