*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Sledgehammer and Nitpick from the command line?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Sun, 29 Jul 2012 11:42:19 -0500*In-reply-to*: <501564A2.7000308@gmx.com>*References*: <501564A2.7000308@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/29/2012 4:27 AM, Jens Doll wrote:

Hello Gottfried, here is a little warning concerning ancient JVMs:I installed I3p on my Win7 64bit machine and it contained an olderJVM, which was also installed. Afterwards the JVM *tried to openports* on my machine and my *printer configuration was corrupted*.

Jens,

* JAVA INCLUDED WITH BOTH CYGWIN & LINUX*

*NORTON QUIT DELETING ISABELLE.EXE*

2) Mature: This file was released 1 month ago. 3) Good: Norton has given this file a favorable ratting.

*OTHER ANTIVIRUS INFORMATION*

*COMPILING PROVERS FOR CYGWIN and E's SLOW STARTUP*

I successfully compiled leo2, satallax, why3, and alt-ergo for Cygwin.

"alt_ergo": A prover error occurred: Unknown input format: tff1

*VAMPIRE 0.6 FOR CYGWIN, INSTALLING LINUX TO GET VAMPIRE* Trying to run Vampire for Cygwin, I get this error: "vampire": A prover error occurred: User error: forced_options is not a valid option The Cygwin version is 0.6, and I assume the Linux version is 1.8.

I got that link off of the satallax web page:

*CREATING 10 FILES TO TEST ONE THEOREM*

Right now, I'm grouping them like this: (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)

(*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*) (*4 satallax leo2*)

Group 3 is mainly the SMT provers.

http://plugins.jedit.org/plugins/?JythonInterpreter http://plugins.jedit.org/plugins/?PythonShell Regards, GB *(THE BATCH FILE, CAN'T BE AN ATTACHMENT)* 12_jedit_set.bat ::Cygwin uses this home set HOME=E:\E_main\02-p\pi\home ::Isabelle uses this home set USER_HOME=/cygdrive/e/E_main/02-p/pi/home ::Various set ISAVERSION=Isabelle2012 set PATH=E:\E_main2\binp\%ISAVERSION%\bin;%PATH% set CHERE_INVOKING=true

set JEDITOPTIONS=-j -settings=/.isabelle/%ISAVERSION%/jedit%1 ::Get command line arg for bash cd %2 set JEDITFILE=%3

*BASH FILE* 12_jedit_set.bat.bash #!/usr/bin/env bash # ######################################################## # $ISAVERSION is set in the batch file that calls this. ######################################################## printenv

*THEORY FILE* theory z0_2_neg_FO imports z0_2 begin nitpick_params[timeout=172800,sat_solver=Lingeling_JNI,verbose,user_axioms] sledgehammer_params[timeout=172800,verbose,debug=false,isar_proof,provers=" e spass_new remote_vampire remote_e_sine remote_iprover_eq "] (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*)

(*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*) (*4 satallax leo2*)

theorem neg_FO__emS_is_unique --"~(The empty set is unique.)": "~(\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS)" apply(auto) sledgehammer oops end

nitpick_params[timeout=172800,sat_solver=Lingeling_JNI,verbose,user_axioms] sledgehammer_params[timeout=172800,verbose,debug=false,isar_proof,provers=""] (*1 e spass_new remote_vampire remote_e_sine remote_iprover_eq*) (*2 vampire z3_tptp spass metis remote_e_tofof remote_iprover remote_snark*) (*3 z3 yices cvc3 smt alt_ergo remote_waldmeister*) (*4 satallax leo2*) (*5 remote_leo2 remote_satallax remote_e remote_z3_tptp remote_cvc3 remote_z3*)

// Compiles Selected Text with LaTeX in "_temp%T" file. Requires(20040113); // Requires this build of WinEdt to work properly SaveRegisters(1111111111); // Clean Macro writing... CMD('Save'); SetOK(1); // Just in case ... SetErrorFlag(0); StartWorking("Make tester file..."); // Reg 4: default file name number // Reg 5: the tester file name // Reg 0,1,2: Temporary working registers // Reg 9: Stores user's highlighted theorem text // Get Selected Text in %!9 GetSel(1,9); // Get the filename suffix. GetString(`Enter filename number suffix.`,`File number`,"0"); LetReg(4,"%!?"); // for the file name number, like z0.thy LetReg(5,"z%!4"); // the tester file name // Get what test to start at. GetString(`Enter beginning test number.`,`Test number`,"1"); JMP(`TEST%!?`); ///////////////////////////////////////// // THEOREM: FIRST-ORDER SLEDGE GROUP 1 ///////////////////////////////////////// :TEST1:: Prompt("%!5_1_lem_FO.thy in jEdit?",1,4,"","JMP(`TEST2`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_1.thy",1,0) ReadFile("%p\%!5_1.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_1`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_1.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_1_lem_FO.thy"); WrL("theory %!5_1_lem_FO"); WrL("imports %!5_1"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0lem_FO__\1\2",111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_1_lem_FO.thy",0); SubstituteInString("%!1",`**(\*1 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_1_lem_FO.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 1 %p %!5_1_lem_FO.thy|,'',0,0,'%!5_1_lem_FO',0,0); ///////////////////////////////////////// // NEGATION: FIRST-ORDER SLEDGE THE NEG GROUP 1 ///////////////////////////////////////// :TEST2:: Prompt("%!5_2_neg_FO.thy in jEdit?",1,4,"","JMP(`TEST3`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_2.thy",1,0) ReadFile("%p\%!5_2.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_2`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_2.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_2_neg_FO.thy"); WrL("theory %!5_2_neg_FO"); WrL("imports %!5_2"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0neg_FO__\1\2",111,0); //Negate it SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_2_neg_FO.thy",0); SubstituteInString("%!1",`**(\*1 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_2_neg_FO.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 2 %p %!5_2_neg_FO.thy|,'',0,0,'%!5_2_neg_FO',0,0); ///////////////////////////////////////// // THEOREM: FIRST-ORDER SLEDGE GROUP 2 ///////////////////////////////////////// :TEST3:: Prompt("%!5_3_lem_FO.thy in jEdit?",1,4,"","JMP(`TEST4`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_3.thy",1,0) ReadFile("%p\%!5_3.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_3`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_3.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_3_lem_FO.thy"); WrL("theory %!5_3_lem_FO"); WrL("imports %!5_3"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0lem_FO__\1\2",111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_3_lem_FO.thy",0); SubstituteInString("%!1",`**(\*2 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_3_lem_FO.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 3 %p %!5_3_lem_FO.thy|,'',0,0,'%!5_3_lem_FO',0,0); ///////////////////////////////////////// // NEGATION: FIRST-ORDER SLEDGE THE NEG GROUP 2 ///////////////////////////////////////// :TEST4:: Prompt("%!5_4_neg_FO.thy in jEdit?",1,4,"","JMP(`TEST5`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_4.thy",1,0) ReadFile("%p\%!5_4.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_4`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_4.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_4_neg_FO.thy"); WrL("theory %!5_4_neg_FO"); WrL("imports %!5_4"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0neg_FO__\1\2",111,0); //Negate it SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_4_neg_FO.thy",0); SubstituteInString("%!1",`**(\*2 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_4_neg_FO.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 4 %p %!5_4_neg_FO.thy|,'',0,0,'%!5_4_neg_FO',0,0); ///////////////////////////////////////// // NITPICK THE THEOREM (set up for satallax leo2) ///////////////////////////////////////// :TEST5:: Prompt("%!5_5_lem_NIT.thy in jEdit?",1,4,"","JMP(`TEST6`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_5.thy",1,0) ReadFile("%p\%!5_5.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_5`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_5.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_5_lem_NIT.thy"); WrL("theory %!5_5_lem_NIT"); WrL("imports %!5_5"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0lem_NIT__\1\2",111,0); WrL("%!0"); WrL(| nitpick|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_5_lem_NIT.thy",0); SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_5_lem_NIT.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 5 %p %!5_5_lem_NIT.thy|,'',0,0,'%!5_5_lem_NIT',0,0); ///////////////////////////////////////// // NITPICK THE NEGATION (set up for satallax leo2) ///////////////////////////////////////// :TEST6:: Prompt("%!5_6_neg_NIT.thy in jEdit?",1,4,"","JMP(`TEST7`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_6.thy",1,0) ReadFile("%p\%!5_6.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_6`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_6.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_6_neg_NIT.thy"); WrL("theory %!5_6_neg_NIT"); WrL("imports %!5_6"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0neg_NIT__\1\2",111,0); //Negate it SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0); WrL("%!0"); WrL(| nitpick|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_6_neg_NIT.thy",0); SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_6_neg_NIT.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 6 %p %!5_6_neg_NIT.thy|,'',0,0,'%!5_6_neg_NIT',0,0); ///////////////////////////////////////// // THEOREM: SMT SLEDGE THE THEOREM ///////////////////////////////////////// :TEST7:: Prompt("%!5_7_lem_SMT.thy in jEdit?",1,4,"","JMP(`TEST8`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_7.thy",1,0) ReadFile("%p\%!5_7.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_7`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_7.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_7_lem_SMT.thy"); WrL("theory %!5_7_lem_SMT"); WrL("imports %!5_7"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0lem_SMT__\1\2",111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_7_lem_SMT.thy",0); SubstituteInString("%!1",`**(\*3 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_7_lem_SMT.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 7 %p %!5_7_lem_SMT.thy|,'',0,0,'%!5_7_lem_SMT',0,0); ///////////////////////////////////////// // NEGATION: SMT SLEDGE THE NEG ///////////////////////////////////////// :TEST8:: Prompt("%!5_8_neg_SMT.thy in jEdit?",1,4,"","JMP(`TEST9`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_8.thy",1,0) ReadFile("%p\%!5_8.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_8`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_8.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_8_neg_SMT.thy"); WrL("theory %!5_8_neg_SMT"); WrL("imports %!5_8"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0neg_SMT__\1\2",111,0); //Negate it SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_8_neg_SMT.thy",0); SubstituteInString("%!1",`**(\*3 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_8_neg_SMT.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 8 %p %!5_8_neg_SMT.thy|,'',0,0,'%!5_8_neg_SMT',0,0); ///////////////////////////////////////// // THEOREM: HOL SLEDGE THE THEOREM ///////////////////////////////////////// :TEST9:: Prompt("%!5_9_lem_HOL.thy in jEdit?",1,4,"","JMP(`TEST10`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_9.thy",1,0) ReadFile("%p\%!5_9.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_9`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_9.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_9_lem_HOL.thy"); WrL("theory %!5_9_lem_HOL"); WrL("imports %!5_9"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0lem_HOL__\1\2",111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_9_lem_HOL.thy",0); SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_9_lem_HOL.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 9 %p %!5_9_lem_HOL.thy|,'',0,0,'%!5_9_lem_HOL',0,0); ///////////////////////////////////////// // NEGATION: HOL SLEDGE THE NEG ///////////////////////////////////////// :TEST10:: Prompt("%!5_10_neg_HOL.thy in jEdit?",1,4,"","JMP(`Exit`);","JMP(`Exit`);"); // create import file from the main file CopyFile("%p\%n.thy", "%p\%!5_10.thy",1,0) ReadFile("%p\%!5_10.thy",0); SubstituteInString("%!0",`theory+[ ]\(0+[a-zA-Z0-9_]\)`,`theory %!5_10`,111,0); SubstituteInString("%!0",`"\.\.*/pi/I"`,``,111,0); WriteFile("%p\%!5_10.thy","%!0"); // create the particular test file OpenOutput("%p\%!5_10_neg_HOL.thy"); WrL("theory %!5_10_neg_HOL"); WrL("imports %!5_10"); WrL("begin"); // Put in nitpick params, sledge params, and commented out provers ReadFile("%b\Macros\+isar-sml\util\NiSl.edt",1); WrL("%!1"); // put the theorem in SubstituteInString("%!9","> \(0{theorem|lemma}+[ ]\)> \(1+[0-9a-zA-Z_'^\\\<\>]\)> \(2+[ :\-]\)> ","\0neg_HOL__\1\2",111,0); //Negate it SubstituteInString("%!0",`"\(0*\)"`,`"\~(\0)"`,111,0); WrL("%!0"); WrL(" apply(auto)"); WrL(| sledgehammer|); WrL(| oops|); WrL("end"); WrL; CloseOutput; // Put the right group of provers in from %!1 above ReadFile("%p\%!5_10_neg_HOL.thy",0); SubstituteInString("%!1",`**(\*4 \(0**\)\*)**`,` \0`,111,1); //delete what I don't want SubstituteInString("%!0",`\(0provers="\)**\(1"]\)`,`\0>%!1>\1`,111,0); WriteFile("%p\%!5_10_neg_HOL.thy","%!0"); Run(|%@('2p');\pi\home\bin\12_jedit_set.bat 10 %p %!5_10_neg_HOL.thy|,'',0,0,'%!5_10_neg_HOL',0,0); Prompt("Done. Open Explorer?",1,4,"Run('%b\Macros\Open\explorer.bat %p','%p',0,0,'Explorer',1,1);","","JMP(`Exit`);"); :Exit:: End;

- Previous by Date: Re: [isabelle] Fun vs Primrec: difference?
- Next by Date: [isabelle] Using Formal_Power_Series.thy
- Previous by Thread: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Thread: [isabelle] Some more project announcements
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list