equal
deleted
inserted
replaced
2969 {\out Level 1} |
2969 {\out Level 1} |
2970 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
2970 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
2971 {\out No subgoals!} |
2971 {\out No subgoals!} |
2972 \end{ttbox} |
2972 \end{ttbox} |
2973 If you run this example interactively, make sure your current theory contains |
2973 If you run this example interactively, make sure your current theory contains |
2974 theory \texttt{Set}, for example by executing |
2974 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. |
2975 \ttindex{set_current_thy}~{\tt"Set"}. Otherwise the default claset may not |
2975 Otherwise the default claset may not contain the rules for set theory. |
2976 contain the rules for set theory. |
|
2977 \index{higher-order logic|)} |
2976 \index{higher-order logic|)} |
2978 |
2977 |
2979 %%% Local Variables: |
2978 %%% Local Variables: |
2980 %%% mode: latex |
2979 %%% mode: latex |
2981 %%% TeX-master: "logics" |
2980 %%% TeX-master: "logics" |