Mercurial Mercurial > hg > nominal2 / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IsaMakefile
author Christian Urban <urbanc@in.tum.de>
Thu, 04 Oct 2012 11:10:23 +0100 (2012-10-04)
changeset 3200 995d47b09ab4
parent 3186 425b4c406d80
child 3208 da575186d492
permissions -rw-r--r--
removed fork_mono flag
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
     1
 












853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     2


## targets













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     3









3111






60c4c93b30d5
made all papers work again



Christian Urban <urbanc@in.tum.de>


parents: 
3110

diff
changeset




     4


default: session








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     5


images: 













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     6









3112






e4050732ba15
tuned make-file



Christian Urban <urbanc@in.tum.de>


parents: 
3111

diff
changeset




     7


all: tests esop pearl pearl-jv qpaper qpaper-jv slides lmcs








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     8














853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     9














853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    10


## global settings













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    11














853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    12


SRC = $(ISABELLE_HOME)/src













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    13


OUT = $(ISABELLE_OUTPUT)













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    14


LOG = $(OUT)/log













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    15









3110






62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    16


USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -m no_brackets













62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    17














62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    18


## Nominal2                                                                                                             













62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    19














62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    20


session: $(LOG)/HOL-Nominal2.gz













62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    21














62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    22


$(LOG)/HOL-Nominal2.gz: Nominal/FROOT.ML Nominal/*.thy













62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    23


	@cd Nominal; $(USEDIR) -f FROOT.ML -b -d "" HOL Nominal2








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    24














853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    25









3110






62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    26


## tests








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    27









3112






e4050732ba15
tuned make-file



Christian Urban <urbanc@in.tum.de>


parents: 
3111

diff
changeset




    28


tests: $(LOG)/HOL-Nominal2-tests.gz








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    29









3110






62e1d888aacc
added a session entry in order to quickly build the heap file (tests took too long)



Christian Urban <urbanc@in.tum.de>


parents: 
3082

diff
changeset




    30


$(LOG)/HOL-Nominal2-tests.gz: Nominal/ROOT.ML Nominal/*.thy








3112






e4050732ba15
tuned make-file



Christian Urban <urbanc@in.tum.de>


parents: 
3111

diff
changeset




    31


	@$(USEDIR) HOL Nominal








3132






87eca760dcba
updated tutorial to latest version and added it to the tests



Christian Urban <urbanc@in.tum.de>


parents: 
3121

diff
changeset




    32


	@$(USEDIR) HOL Tutorial








3200






995d47b09ab4
removed fork_mono flag



Christian Urban <urbanc@in.tum.de>


parents: 
3186

diff
changeset




    33


#	@$(USEDIR) HOL Nominal/Ex/CPS








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    34









2748






6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




    35


## ESOP Paper








1772






48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    36









2748






6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




    37


esop: $(LOG)/HOL-ESOP-Paper.gz








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    38









2748






6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




    39


$(LOG)/HOL-ESOP-Paper.gz: ESOP-Paper/ROOT.ML ESOP-Paper/document/root.* ESOP-Paper/*.thy








2749






7cf2d79d8d5e
tuned IsaMakefile



Christian Urban <urbanc@in.tum.de>


parents: 
2748

diff
changeset




    40


	@$(USEDIR) -f ROOT.ML -D generated Nominal2 ESOP-Paper








2748






6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




    41


	$(ISABELLE_TOOL) document -o pdf  ESOP-Paper/generated













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




    42


	@cp ESOP-Paper/document.pdf esop-paper.pdf








1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    43









2985






05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    44


## LMCS Paper













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    45














05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    46


lmcs: $(LOG)/HOL-LMCS-Paper.gz













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    47














05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    48


$(LOG)/HOL-LMCS-Paper.gz: LMCS-Paper/ROOT.ML LMCS-Paper/document/root.* LMCS-Paper/*.thy













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    49


	@$(USEDIR) -f ROOT.ML -D generated Nominal2 LMCS-Paper













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    50


	$(ISABELLE_TOOL) document -o pdf  LMCS-Paper/generated













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    51


	@cp LMCS-Paper/document.pdf lmcs-paper.pdf













05ccb61aa628
started lmcs paper (isabelle make lmcs)



Christian Urban <urbanc@in.tum.de>


parents: 
2856

diff
changeset




    52









1785






95df71c3df2f
added new paper directory for further work



Christian Urban <urbanc@in.tum.de>


parents: 
1775

diff
changeset




    53


## Pearl Paper ITP








1772






48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    54














48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    55


pearl: $(LOG)/HOL-Pearl.gz













48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    56









1775






86122d793f32
typos in paper



Christian Urban <urbanc@in.tum.de>


parents: 
1774

diff
changeset




    57


$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy








1772






48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    58


	@$(USEDIR) -D generated HOL Pearl













48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    59


	$(ISABELLE_TOOL) document -o pdf Pearl/generated













48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    60


	@cp Pearl/document.pdf pearl.pdf













48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    61









1785






95df71c3df2f
added new paper directory for further work



Christian Urban <urbanc@in.tum.de>


parents: 
1775

diff
changeset




    62


## Pearl Journal Paper 













95df71c3df2f
added new paper directory for further work



Christian Urban <urbanc@in.tum.de>


parents: 
1775

diff
changeset




    63









2742






f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    64


$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Nominal/*.thy













f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    65


	@cd Pearl-jv; $(USEDIR) -b -f ROOT.ML HOL HOL-Pearl-jv








1785






95df71c3df2f
added new paper directory for further work



Christian Urban <urbanc@in.tum.de>


parents: 
1775

diff
changeset




    66









2742






f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    67


pearl-jv: $(LOG)/HOL-Pearl-jv.gz Pearl-jv/ROOT2.ML Pearl-jv/document/root.* Pearl-jv/*.thy













f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    68


	@$(USEDIR) -f ROOT2.ML -D generated HOL-Pearl-jv Pearl-jv













f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    69


	@$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated













f1192e3474e0
more on the paper



Christian Urban <urbanc@in.tum.de>


parents: 
2524

diff
changeset




    70


	@cp Pearl-jv/document.pdf pearl-jv.pdf	








1772






48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




    71









1975






b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    72


## Quotient Paper 













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    73














b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    74


qpaper: $(LOG)/HOL-QPaper.gz













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    75














b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    76


$(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    77


	@$(USEDIR) -D generated HOL Quotient-Paper













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    78


	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    79


	@cp Quotient-Paper/document.pdf qpaper.pdf













b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




    80









3082






a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    81


## Quotient Journal Paper













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    82














a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    83


qpaper-jv: $(LOG)/HOL-QPaper-jv.gz













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    84














a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    85


$(LOG)/HOL-QPaper-jv.gz: Quotient-Paper-jv/ROOT.ML Quotient-Paper-jv/document/root.* Quotient-Paper-jv/*.thy













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    86


	@$(USEDIR) -D generated HOL Quotient-Paper-jv













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    87


	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    88


	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf













a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
3052

diff
changeset




    89









3173






9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    90


## SFT Paper













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    91














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    92


sft-paper: $(LOG)/Nominal-SFT-Paper.gz













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    93














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    94


$(LOG)/Nominal-SFT-Paper.gz: Nominal/Ex/SFT/ROOT.ML Nominal/Ex/SFT/document/root.* Nominal/Ex/SFT/*.thy













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    95


	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/SFT













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    96


	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/SFT/generated













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    97


	@cp Nominal/Ex/SFT/document.pdf sft-paper.pdf













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    98














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




    99














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   100


## Exec Paper













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   101














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   102


exec-paper: $(LOG)/Nominal-Exec-Paper.gz













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   103














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   104


$(LOG)/Nominal-Exec-Paper.gz: Nominal/Ex/Exec/ROOT.ML Nominal/Ex/Exec/document/root.* Nominal/Ex/Exec/*.thy













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   105


	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/Exec













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   106


	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/Exec/generated













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   107


	@cp Nominal/Ex/Exec/document.pdf exec-paper.pdf













9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   108














9876d73adb2b
Executing Lambda Terms



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 
3132

diff
changeset




   109









2856






e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   110


## Nominal Functions paper













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   111














e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   112


fnpaper: $(LOG)/HOL-FnPaper.gz













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   113














e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   114


$(LOG)/HOL-FnPaper.gz: Fun-Paper/ROOT.ML Fun-Paper/document/root.* Fun-Paper/*.thy













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   115


	@$(USEDIR) -D generated HOL Fun-Paper













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   116


	$(ISABELLE_TOOL) document -o pdf Fun-Paper/generated













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   117


	@cp Fun-Paper/document.pdf fnpaper.pdf













e36beb11723c
added a stub for function paper; "isabelle make fnpaper"



Christian Urban <urbanc@in.tum.de>


parents: 
2786

diff
changeset




   118









2299






09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   119


## Slides













09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   120









2351






842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   121


session1: Slides/ROOT1.ML \








2299






09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   122


         Slides/document/root* \













09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   123


         Slides/Slides1.thy








2351






842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   124


	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides








2299






09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   125














09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   126


slides1: session1













09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   127


	rm -f Slides/generated1/*.aux # otherwise latex will fall over













09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   128


	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   129


	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex








2351






842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   130


	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf     













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   131














842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   132


session2: Slides/ROOT2.ML \













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   133


         Slides/document/root* \













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   134


         Slides/Slides2.thy













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   135


	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   136














842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   137


slides2: session2













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   138


	rm -f Slides/generated2/*.aux # otherwise latex will fall over













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   139


	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   140


	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   141


	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf 













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   142














842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   143


session3: Slides/ROOT3.ML \













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   144


         Slides/document/root* \













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   145


         Slides/Slides3.thy













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   146


	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   147














842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   148


slides3: session3













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   149


	rm -f Slides/generated3/*.aux # otherwise latex will fall over













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   150


	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   151


	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













842969a598f2
added material for slides



Christian Urban <urbanc@in.tum.de>


parents: 
2299

diff
changeset




   152


	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf 








2299






09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   153









2459






ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   154


session4: Slides/ROOT4.ML \













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   155


         Slides/document/root* \













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   156


         Slides/Slides4.thy













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   157


	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   158














ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   159


slides4: session4













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   160


	rm -f Slides/generated4/*.aux # otherwise latex will fall over













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   161


	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   162


	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   163


	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf 













ac3470e1e5af
slides of my talk



Christian Urban <urbanc@in.tum.de>


parents: 
2454

diff
changeset




   164









2748






6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   165


session5: Slides/ROOT5.ML \













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   166


         Slides/document/root* \













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   167


         Slides/Slides5.thy













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   168


	@$(USEDIR) -D generated5 -f ROOT5.ML HOL-Nominal Slides













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   169














6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   170


slides5: session5













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   171


	rm -f Slides/generated5/*.aux # otherwise latex will fall over













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   172


	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   173


	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   174


	cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf 













6f38e357b337
rearranged directories and updated to new Isabelle



Christian Urban <urbanc@in.tum.de>


parents: 
2742

diff
changeset




   175









2762






1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   176


session6: Slides/ROOT6.ML \













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   177


         Slides/document/root* \













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   178


         Slides/Slides6.thy













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   179


	@$(USEDIR) -D generated6 -f ROOT6.ML HOL-Nominal Slides













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   180














1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   181


slides6: session6













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   182


	rm -f Slides/generated6/*.aux # otherwise latex will fall over













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   183


	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   184


	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   185


	cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf 













1a1a2b778ba2
Shanghai slides



Christian Urban <urbanc@in.tum.de>


parents: 
2749

diff
changeset




   186









2772






c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   187


session7: Slides/ROOT7.ML \













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   188


         Slides/document/root* \













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   189


         Slides/Slides6.thy













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   190


	@$(USEDIR) -D generated7 -f ROOT7.ML HOL Slides













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   191














c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   192


slides7: session7













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   193


	rm -f Slides/generated7/*.aux # otherwise latex will fall over                                      













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   194


	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   195


	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   196


	cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf 













c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   197









2785






c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   198


session8: Slides/ROOT8.ML \













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   199


         Slides/document/root* \













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   200


         Slides/Slides6.thy








2786






bccda961a612
more on slides



Christian Urban <urbanc@in.tum.de>


parents: 
2785

diff
changeset




   201


	@$(USEDIR) -D generated8 -f ROOT8.ML HOL-Nominal Slides








2772






c3ff26204d2a
added slides for beijing



Christian Urban <urbanc@in.tum.de>


parents: 
2762

diff
changeset




   202









2785






c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   203


slides8: session8













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   204


	rm -f Slides/generated8/*.aux # otherwise latex will fall over                                      













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   205


	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   206


	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   207


	cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf 













c63ffe1735eb
added slides for copenhagen



Christian Urban <urbanc@in.tum.de>


parents: 
2772

diff
changeset




   208









3052






41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   209


session9: Slides/ROOT9.ML \













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   210


         Slides/document/root* \













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   211


         Slides/Slides6.thy













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   212


	@$(USEDIR) -D generated9 -f ROOT9.ML HOL-Nominal Slides













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   213














41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   214


slides9: session9













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   215


	rm -f Slides/generated9/*.aux # otherwise latex will fall over                                      













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   216


	cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   217


	cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   218


	cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf 













41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   219









3121






878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   220


sessionA: Slides/ROOTA.ML \













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   221


	Slides/document/root* \













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   222


	Slides/SlidesA.thy













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   223


	@$(USEDIR) -D generatedA -f ROOTA.ML HOL-Nominal Slides








3052






41ec301eb062
slides for talk in Leicester



Christian Urban <urbanc@in.tum.de>


parents: 
2996

diff
changeset




   224









3121






878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   225


slidesA: sessionA













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   226


	rm -f Slides/generatedA/*.aux # otherwise latex will fall over













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   227


	cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   228


	cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   229


	cp Slides/generatedA/root.beamer.pdf Slides/slidesA.pdf 













878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   230














878de0084b62
added fs and pt for multisets



Christian Urban <urbanc@in.tum.de>


parents: 
3112

diff
changeset




   231


slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9 slidesA








2299






09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   232














09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   233














09bbed4f21d6
added slides



Christian Urban <urbanc@in.tum.de>


parents: 
1975

diff
changeset




   234









1975






b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper



Christian Urban <urbanc@in.tum.de>


parents: 
1785

diff
changeset




   235









1261






853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   236


## clean













853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   237














853abc14c5c6
added IsaMakefile...but so far included only a test for the parser



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   238


clean:








1772






48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory



Christian Urban <urbanc@in.tum.de>


parents: 
1491

diff
changeset




   239


	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz 















nominal2