equal
deleted
inserted
replaced
211 simplify (simpset_of ctxt delsimps[@{thm not_None_eq}]) |
211 simplify (simpset_of ctxt delsimps[@{thm not_None_eq}]) |
212 (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] |
212 (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] |
213 *} |
213 *} |
214 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
214 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) |
215 |
215 |
216 translations |
|
217 "option"<= (type) "Option.option" |
|
218 "list" <= (type) "List.list" |
|
219 "sum3" <= (type) "Basis.sum3" |
|
220 |
|
221 |
216 |
222 section "quantifiers for option type" |
217 section "quantifiers for option type" |
223 |
218 |
224 syntax |
219 syntax |
225 "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) |
220 "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) |