equal
deleted
inserted
replaced
254 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
254 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] |
255 *} |
255 *} |
256 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
256 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
257 |
257 |
258 translations |
258 translations |
259 "option"<= (type) "Option.option" |
259 "option"<= (type) "Datatype.option" |
260 "list" <= (type) "List.list" |
260 "list" <= (type) "List.list" |
261 "sum3" <= (type) "Basis.sum3" |
261 "sum3" <= (type) "Basis.sum3" |
262 |
262 |
263 |
263 |
264 section "quantifiers for option type" |
264 section "quantifiers for option type" |