equal
deleted
inserted
replaced
234 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
234 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
235 *} |
235 *} |
236 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
236 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
237 |
237 |
238 translations |
238 translations |
239 "option"<= (type) "Option.option" |
239 "option"<= (type) "Datatype.option" |
240 "list" <= (type) "List.list" |
240 "list" <= (type) "List.list" |
241 "sum3" <= (type) "Basis.sum3" |
241 "sum3" <= (type) "Basis.sum3" |
242 |
242 |
243 |
243 |
244 section "quantifiers for option type" |
244 section "quantifiers for option type" |