equal
deleted
inserted
replaced
90 (("nthel1", "limited_nthel1"), "lim_typing")], |
90 (("nthel1", "limited_nthel1"), "lim_typing")], |
91 manual_reorder = []}) *} |
91 manual_reorder = []}) *} |
92 |
92 |
93 lemma |
93 lemma |
94 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
94 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
95 quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
95 quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
96 oops |
96 oops |
97 |
97 |
98 text {* Verifying that the found counterexample really is one by means of a proof *} |
98 text {* Verifying that the found counterexample really is one by means of a proof *} |
99 |
99 |
100 lemma |
100 lemma |