equal
deleted
inserted
replaced
1978 Scan.succeed (K (SIMPLE_METHOD' |
1978 Scan.succeed (K (SIMPLE_METHOD' |
1979 (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))) |
1979 (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))) |
1980 *} "solve goal by normalization" |
1980 *} "solve goal by normalization" |
1981 |
1981 |
1982 |
1982 |
|
1983 (* |
1983 subsection {* Try *} |
1984 subsection {* Try *} |
1984 |
1985 |
1985 setup {* Try.setup *} |
1986 setup {* Try.setup *} |
|
1987 *) |
1986 |
1988 |
1987 subsection {* Counterexample Search Units *} |
1989 subsection {* Counterexample Search Units *} |
1988 |
1990 |
1989 subsubsection {* Quickcheck *} |
1991 subsubsection {* Quickcheck *} |
1990 |
1992 |