IsaMakefile
changeset 3173 9876d73adb2b
parent 3132 87eca760dcba
child 3186 425b4c406d80
equal deleted inserted replaced
3172:4cf3a4d36799 3173:9876d73adb2b
    83 
    83 
    84 $(LOG)/HOL-QPaper-jv.gz: Quotient-Paper-jv/ROOT.ML Quotient-Paper-jv/document/root.* Quotient-Paper-jv/*.thy
    84 $(LOG)/HOL-QPaper-jv.gz: Quotient-Paper-jv/ROOT.ML Quotient-Paper-jv/document/root.* Quotient-Paper-jv/*.thy
    85 	@$(USEDIR) -D generated HOL Quotient-Paper-jv
    85 	@$(USEDIR) -D generated HOL Quotient-Paper-jv
    86 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated
    86 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated
    87 	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf
    87 	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf
       
    88 
       
    89 ## SFT Paper
       
    90 
       
    91 sft-paper: $(LOG)/Nominal-SFT-Paper.gz
       
    92 
       
    93 $(LOG)/Nominal-SFT-Paper.gz: Nominal/Ex/SFT/ROOT.ML Nominal/Ex/SFT/document/root.* Nominal/Ex/SFT/*.thy
       
    94 	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/SFT
       
    95 	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/SFT/generated
       
    96 	@cp Nominal/Ex/SFT/document.pdf sft-paper.pdf
       
    97 
       
    98 
       
    99 ## Exec Paper
       
   100 
       
   101 exec-paper: $(LOG)/Nominal-Exec-Paper.gz
       
   102 
       
   103 $(LOG)/Nominal-Exec-Paper.gz: Nominal/Ex/Exec/ROOT.ML Nominal/Ex/Exec/document/root.* Nominal/Ex/Exec/*.thy
       
   104 	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/Exec
       
   105 	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/Exec/generated
       
   106 	@cp Nominal/Ex/Exec/document.pdf exec-paper.pdf
       
   107 
    88 
   108 
    89 ## Nominal Functions paper
   109 ## Nominal Functions paper
    90 
   110 
    91 fnpaper: $(LOG)/HOL-FnPaper.gz
   111 fnpaper: $(LOG)/HOL-FnPaper.gz
    92 
   112