equal
deleted
inserted
replaced
998 lemma "Q (Eps Q)" |
998 lemma "Q (Eps Q)" |
999 nitpick [expect = genuine] |
999 nitpick [expect = genuine] |
1000 oops |
1000 oops |
1001 |
1001 |
1002 lemma "(Q\<Colon>nat set) (Eps Q)" |
1002 lemma "(Q\<Colon>nat set) (Eps Q)" |
1003 nitpick [expect = none] |
1003 nitpick [expect = none] (* unfortunate *) |
1004 oops |
1004 oops |
1005 |
1005 |
1006 lemma "\<not> Q (Eps Q)" |
1006 lemma "\<not> Q (Eps Q)" |
1007 nitpick [expect = genuine] |
1007 nitpick [expect = genuine] |
1008 oops |
1008 oops |
1051 nitpick [expect = genuine] |
1051 nitpick [expect = genuine] |
1052 oops |
1052 oops |
1053 |
1053 |
1054 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)" |
1054 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)" |
1055 nitpick [expect = none] |
1055 nitpick [expect = none] |
1056 oops |
1056 sorry |
1057 |
1057 |
1058 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
1058 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
1059 nitpick [expect = none] |
1059 nitpick [expect = none] |
1060 oops |
1060 sorry |
1061 |
1061 |
1062 subsection {* Destructors and Recursors *} |
1062 subsection {* Destructors and Recursors *} |
1063 |
1063 |
1064 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
1064 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
1065 nitpick [card = 2, expect = none] |
1065 nitpick [card = 2, expect = none] |