equal
deleted
inserted
replaced
22 Word |
22 Word |
23 "~~/src/HOL/ex/Commutative_Ring_Complete" |
23 "~~/src/HOL/ex/Commutative_Ring_Complete" |
24 "~~/src/HOL/ex/Records" |
24 "~~/src/HOL/ex/Records" |
25 begin |
25 begin |
26 |
26 |
|
27 lemma [code, code del]: "(term_of \<Colon> 'a Predicate.pred \<Rightarrow> term) = term_of" .. |
|
28 |
27 text {* However, some aren't executable *} |
29 text {* However, some aren't executable *} |
28 |
30 |
29 declare pair_leq_def[code del] |
31 declare pair_leq_def[code del] |
30 declare max_weak_def[code del] |
32 declare max_weak_def[code del] |
31 declare min_weak_def[code del] |
33 declare min_weak_def[code del] |