equal
deleted
inserted
replaced
1995 method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *} |
1995 method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *} |
1996 "solve goal by evaluation" |
1996 "solve goal by evaluation" |
1997 |
1997 |
1998 method_setup normalization = {* |
1998 method_setup normalization = {* |
1999 Scan.succeed (K (SIMPLE_METHOD' |
1999 Scan.succeed (K (SIMPLE_METHOD' |
2000 (CHANGED_PROP o CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))) |
2000 (CHANGED_PROP o (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))) |
2001 *} "solve goal by normalization" |
2001 *} "solve goal by normalization" |
2002 |
2002 |
2003 |
2003 |
2004 subsection {* Counterexample Search Units *} |
2004 subsection {* Counterexample Search Units *} |
2005 |
2005 |