equal
deleted
inserted
replaced
96 *} |
96 *} |
97 |
97 |
98 apply(erule lfp_induct_set) |
98 apply(erule lfp_induct_set) |
99 apply(rule mono_ef) |
99 apply(rule mono_ef) |
100 apply(simp) |
100 apply(simp) |
101 (*pr(latex xsymbols symbols);*) |
|
102 txt{*\noindent |
101 txt{*\noindent |
103 Having disposed of the monotonicity subgoal, |
102 Having disposed of the monotonicity subgoal, |
104 simplification leaves us with the following goal: |
103 simplification leaves us with the following goal: |
105 \begin{isabelle} |
104 \begin{isabelle} |
106 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline |
105 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline |