tuned CASC method
authorblanchet
Mon, 06 Jun 2011 20:36:34 +0200
changeset 43161 27dcda8fc89b
parent 43160 d4f347508cd4
child 43162 9a8acc5adfa3
tuned CASC method
src/HOL/ex/CASC_Setup.thy
--- a/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:34 2011 +0200
@@ -63,8 +63,8 @@
 *}
 
 method_setup isabellep = {*
-  Scan.lift Parse.nat >>
+  Scan.lift (Scan.optional Parse.nat 1) >>
     (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
-*} ""
+*} "combination of Isabelle provers and oracles for CASC"
 
 end