1.1 --- a/.hgignore Thu Mar 10 12:45:58 2011 +0100
1.2 +++ b/.hgignore Thu Mar 10 15:12:55 2011 +0100
1.3 @@ -7,6 +7,7 @@
1.4
1.5 *.tgz
1.6 *.orig
1.7 +*.ps
1.8
1.9 syntax: regexp
1.10
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/bin/isac_jedit Thu Mar 10 15:12:55 2011 +0100
2.3 @@ -0,0 +1,13 @@
2.4 +#!/usr/bin/env bash
2.5 +cd src/Pure/
2.6 +echo "Building Pure.jar"
2.7 +../../bin/isabelle env ./build-jars
2.8 +echo "copying Pure.jar to contrib/jedit"
2.9 +cp ../../lib/classes/Pure.jar ../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/
2.10 +echo "Building Isac.jar"
2.11 +cd /home/gadei/jedit-isac/isac/src/Tools/isac/jEdit
2.12 +ant jar
2.13 +cd /home/gadei/jedit-isac/isac/src/Pure/
2.14 +echo "copying Isac.jar to contrib/jedit"
2.15 +cp ../Tools/isac/jEdit/contrib/jEdit/build/jars/Isac.jar ../../contrib/jedit-4.3.2_Isabelle-6d736d983d5c/jars/
2.16 +echo "Done!"
3.1 --- a/doc-src/isac/Protokoll_Steger_Marco/Protokoll.ps Thu Mar 10 12:45:58 2011 +0100
3.2 +++ b/doc-src/isac/Protokoll_Steger_Marco/Protokoll.ps Thu Mar 10 15:12:55 2011 +0100
3.3 @@ -1,17 +1,17 @@
3.4 %!PS-Adobe-2.0
3.5 %%Creator: dvips(k) 5.98 Copyright 2009 Radical Eye Software
3.6 %%Title: Protokoll.dvi
3.7 -%%CreationDate: Tue Mar 1 16:49:27 2011
3.8 -%%Pages: 2
3.9 +%%CreationDate: Wed Mar 2 09:25:33 2011
3.10 +%%Pages: 4
3.11 %%PageOrder: Ascend
3.12 %%BoundingBox: 0 0 596 842
3.13 -%%DocumentFonts: Times-Roman Times-Bold
3.14 +%%DocumentFonts: Times-Roman Times-Bold CMSY10
3.15 %%DocumentPaperSizes: a4
3.16 %%EndComments
3.17 %DVIPSWebPage: (www.radicaleye.com)
3.18 %DVIPSCommandLine: dvips -o Protokoll.ps Protokoll.dvi
3.19 %DVIPSParameters: dpi=600
3.20 -%DVIPSSource: TeX output 2011.03.01:1649
3.21 +%DVIPSSource: TeX output 2011.03.02:0925
3.22 %%BeginProcSet: tex.pro 0 0
3.23 %!
3.24 /TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
3.25 @@ -221,24 +221,265 @@
3.26 end
3.27
3.28 %%EndProcSet
3.29 +%%BeginFont: CMSY10
3.30 +%!PS-AdobeFont-1.0: CMSY10 003.002
3.31 +%%Title: CMSY10
3.32 +%Version: 003.002
3.33 +%%CreationDate: Mon Jul 13 16:17:00 2009
3.34 +%%Creator: David M. Jones
3.35 +%Copyright: Copyright (c) 1997, 2009 American Mathematical Society
3.36 +%Copyright: (<http://www.ams.org>), with Reserved Font Name CMSY10.
3.37 +% This Font Software is licensed under the SIL Open Font License, Version 1.1.
3.38 +% This license is in the accompanying file OFL.txt, and is also
3.39 +% available with a FAQ at: http://scripts.sil.org/OFL.
3.40 +%%EndComments
3.41 +FontDirectory/CMSY10 known{/CMSY10 findfont dup/UniqueID known{dup
3.42 +/UniqueID get 5096651 eq exch/FontType get 1 eq and}{pop false}ifelse
3.43 +{save true}{false}ifelse}{false}ifelse
3.44 +11 dict begin
3.45 +/FontType 1 def
3.46 +/FontMatrix [0.001 0 0 0.001 0 0 ]readonly def
3.47 +/FontName /CMSY10 def
3.48 +/FontBBox {-29 -960 1116 775 }readonly def
3.49 +/UniqueID 5096651 def
3.50 +/PaintType 0 def
3.51 +/FontInfo 9 dict dup begin
3.52 +/version (003.002) readonly def
3.53 +/Notice (Copyright \050c\051 1997, 2009 American Mathematical Society \050<http://www.ams.org>\051, with Reserved Font Name CMSY10.) readonly def
3.54 +/FullName (CMSY10) readonly def
3.55 +/FamilyName (Computer Modern) readonly def
3.56 +/Weight (Medium) readonly def
3.57 +/ItalicAngle -14.04 def
3.58 +/isFixedPitch false def
3.59 +/UnderlinePosition -100 def
3.60 +/UnderlineThickness 50 def
3.61 +end readonly def
3.62 +/Encoding 256 array
3.63 +0 1 255 {1 index exch /.notdef put} for
3.64 +dup 15 /bullet put
3.65 +readonly def
3.66 +currentdict end
3.67 +currentfile eexec
3.68 +D9D66F633B846AB284BCF8B0411B772DE5CD06DFE1BE899059C588357426D7A0
3.69 +7B684C079A47D271426064AD18CB9750D8A986D1D67C1B2AEEF8CE785CC19C81
3.70 +DE96489F740045C5E342F02DA1C9F9F3C167651E646F1A67CF379789E311EF91
3.71 +511D0F605B045B279357D6FC8537C233E7AEE6A4FDBE73E75A39EB206D20A6F6
3.72 +1021961B748D419EBEEB028B592124E174CA595C108E12725B9875544955CFFD
3.73 +028B698EF742BC8C19F979E35B8E99CADDDDC89CC6C59733F2A24BC3AF36AD86
3.74 +1319147A4A219ECB92D0D9F6228B51A97C29547000FCC8A581BE543D73F1FED4
3.75 +3D08C53693138003C01E1D216B185179E1856E2A05AA6C66AABB68B7E4409021
3.76 +91AA9D8E4C5FBBDA55F1BB6BC679EABA06BE9795DB920A6343CE934B04D75DF2
3.77 +E0C30B8FD2E475FE0D66D4AA65821864C7DD6AC9939A04094EEA832EAD33DB7A
3.78 +11EE8D595FB0E543D0E80D31D584B97879B3C7B4A85CC6358A41342D70AD0B97
3.79 +C14123421FE8A7D131FB0D03900B392FDA0ABAFC25E946D2251F150EC595E857
3.80 +D17AE424DB76B431366086F377B2A0EEFD3909E3FA35E51886FC318989C1EF20
3.81 +B6F5990F1D39C22127F0A47BC8461F3AFDF87D9BDA4B6C1D1CFD7513F1E3C3D3
3.82 +93BEF764AA832316343F9FE869A720E4AA87AE76FA87A833BBC5892DE05B867F
3.83 +10FA225E233BCFA9BB51F46A6DF22ADCEACC01C3CD1F54C9AEFA25E92EFAC00D
3.84 +7E2BA427C25483BA42A199F4D2E43DFCE79A7156F7417ACF78E41FCA91E6C9EF
3.85 +B933450D851B73A6AB6AEA7EE4C710CB5C14270D1674FA334686653793FCB31B
3.86 +491E870D3C2BC654D2C1DE463EC9BA29D7371AA1078800EF93D3F66263A2EBBB
3.87 +F5723697BF7448BD0D2E301544BECF497FD475B85DFEF52AF4F8F8BE445CABE6
3.88 +019318806D10C5952157FF8F8286C1EE701545C8F60EFA854EAE66835A2046A6
3.89 +915D395F1E0366EFE0C0391583FE001FF16D82A2E2DA5F57754A2C6F69306E36
3.90 +356ECF8EFC3F1188AD6FCD2427E0580C97A5B69B4E0E09B85EEDE142F5ADD2F0
3.91 +5DE51D6DB72B127412A0D57106C19CA493048A4F815129ABE767D51715B1515D
3.92 +9C21067CB5BC88741B7298C83EAE36A866DFA87D8981F179B1C31292F56BBB64
3.93 +3C430779468AAF07C8A8B4934E1E775FE3F35186BD1FA6EE3689C1C750678AF1
3.94 +FBF9B23195A124C5C991FE670AC0C86FD39D2B07B9A319E74EFD498B45820252
3.95 +720ECDF7294F7B0B137CEB86D33BFCEB8606985A3260FD669E461C8BE94216C5
3.96 +D434FD8854F44EE66E5A289A9F9E32BC36AF645D53F96652602BAED418C8D726
3.97 +BD04A1B4617551FE4DEF54083D414F7DCE004E6BB2DC9C2EF7CE232B254BA2C5
3.98 +7DCBD36C2072ED46FF711F121A701E2284BF1B718B3164382B8F453D68FA0377
3.99 +DFE106503B8401D4DB87F5402A3AC9A442FA060B0610A9524D530C7157C26B56
3.100 +AC970FCC1D5655FFFFA39246E6420CF97D08ADFB7B05822679BD40C638DDF0E7
3.101 +A97BFE8918B611A145AC965C203F1428812F9D340AF499B3A915B22BE798594E
3.102 +0F520109FC81E452180AE45B170FF999C5FC2761C6CECD8742A5A6FC97F16743
3.103 +AD4EFCC6572A6D3F3E4E330C5CB2FF6FEA48A5B64DD3DBE943BD9918D4A18E18
3.104 +CBCF598AEFBB6AB3CD2CBC9BFD6099272F6543F3E532E0E21E614BD2880B1023
3.105 +0AC234CB705827BF016DB84E00E8C255FDEFA0101A842929540B7B4AA8A089BD
3.106 +5EFF05B72356B6BC3727817823B5CDBB1B963103000D7F2A4E2A1472FC3E614B
3.107 +5CBCB6D6D784023173DEFEBFA8F9ED87EC1A0A9EE98CA59CFC964CF943DC683F
3.108 +E9E00DA718C4425A705A69D99988EC6F152525C790912C2E46A2381A569424AB
3.109 +54DF4798BC2D7E7A361E7991641D4B756CE2A7FF4A2848927092C59C2C4B8809
3.110 +E13AB84FB6B111E680D7FB9F2FFC2C5C66B0B501E4447C2E46C10E2F6124476F
3.111 +A140C404CFE2DC9E0199BF61E035CEB481D438139A9630934E541D261FFD2906
3.112 +4CAD99E20655FA746AFB81EDBB5601F5FD6B1D6832A01D585E2C55053F6A7378
3.113 +4DAACCAC7608DBDADAAE732D66B3E7F87E79756337C1A961E53A4651BE7C77F4
3.114 +038B89C87F650C54A2A90EB7F1D525BB353F33318551EE8D84A6A83C718EA5A4
3.115 +B2AC0F7306B1E095819B87015A90CA3ED739B09061782C28CDB36BA4BD5E5308
3.116 +5CBB70414E4112193DAC4A1FA30996327230D1E021F3CD8115E12D239D93FFDC
3.117 +B645910EB29E40D830E7BAF2DB255FD7C4E776557BB38157917D993EAC245837
3.118 +A3B515147043574157B8342D829C7228CCEA843ABC89D1785A9672A5923FC4CD
3.119 +2F3FF27E6FCACF84E2D3136CA2C0FD3EF1EE7354CD04C38B5FB874553646ED2D
3.120 +CEDF7E362EADD04B18051F20A8FB0DE18E152385B9D05F98A3A7EF177824E246
3.121 +455ABE69E2F700EB78185CCFC07E3B4C6FA301112528D977367D30D0D5D59EDE
3.122 +FAEB706DDC970A9E296236C725B2B55B09B9C336B8E23CBA5FB8692D56F33B03
3.123 +16294E5FC7FAA42E96395A57CE51CA8DDD77442F142E2E576B778373FB31C81C
3.124 +16840BB422CA827E30A81829648BDF1CA36700EA32AD888D097C1FE0A05B2D9F
3.125 +483AEE40269DF09AF0D1AD3DF80C45DDC59C2A03FBB661C79B87853737C6D352
3.126 +67626B657321B16198DBD6DB98A092F17878AE4698121E1006E53D6F9B0A3BE2
3.127 +3FB68828EF854A0CDBAA68B37ABCA6AD4A3D809AAF0BAB1697A81FE59C98C472
3.128 +1E33CD70A75A22C249DD11D76C2575ED3370A25892A16D2FD569CDA70C130770
3.129 +93F493C7D47D6F9A5424A7A542BAD726BFC3AB225DCEBBE6AC4BE006F8C7C0EA
3.130 +051424B08305BF2D951AB2986AAFEA04E078CA79B399585BFF0F1ADCED02E15B
3.131 +8765EB6BF6A8E4D0901EFF2C3AA104924EAD9637A35D877E0C51A3C37DA78CD4
3.132 +8643C8CE6DCDDE3F116A6C2390F948E5371BEB5AD2E87B41C5F01FB5C196C436
3.133 +6E256A88D082E3F46E4EFFBF605B2EFF1E9D9AD5EE4DDC323A137CD9451EDEE0
3.134 +06F7D82898D71FAF2362C0FCF1F726F97F820305B7CE20728CA08C63575083A7
3.135 +84BA28B7DE2B916432475510E274C12FFD1660A717F51DACFDF0A102D85224E0
3.136 +D6DB607BB72569ABB8A7BC6A10354CBBC01732EFE35B72062DF269CB25EA3DE6
3.137 +DC603B04C90C5912D2C38D7A5ACDCDD3F6F116D884F0D8C528F69D5D47BA20DB
3.138 +0A9E585C7D8CC3C324FE8A1DF150279F7E8FB43BDB720E624E5E9918032C02CD
3.139 +8020636AE5C38DA2484B7F4B34163E0D0A561B43B80E97746DC05C871AB620EC
3.140 +C5D47101ECED4A7E25F291184BEF8B80024AA7BB456C1B83A907652B331DEA34
3.141 +754226C39C6889EBEEFDAD081E01EF8FE47751987667836FDE4C8BB8A3FD4406
3.142 +1E643B4EA37BD370734D1A2DB17C2F4B74B4ED75098B433601F75A88C9A37A05
3.143 +CCB157EF6E32023BFA33973F3E655A4D58289136996FCFA61EEABD70791B6523
3.144 +1FF5DE71AB8A17038923118A5EED8D59C4C58D246FFA9BB26472346B40C8741F
3.145 +153D19CAFF20DD2A86C6DB89154A630FB1761929FC3F0448EE2F089C1C953E02
3.146 +905BA8DE75D101A982A611056C4B237596C10951DD98BAB838B742D3CF7DE718
3.147 +617DB72E5268583223E37E029D1C8FD3F1D21690151F76B76C52C725CA135CA2
3.148 +8666553E863CE188BFC9B99AF56AC2DB5BFEBEB12FB563D00244EB89E478657A
3.149 +98AF2E1223C1ABC25A4500E8119B86EB3C26B8A2F3505A3E5610F89B7C34E278
3.150 +53FA0A54A7F46D84A35EFEC36AE660A9E3C37EE3864106702DE5AF6C45ABF64B
3.151 +888A4A51323138CE77DB935576FE6B4824B6942DF80625098CE1B5B32B234F1D
3.152 +052A9D6039697118A9D793793775D8729D8574A2E74D7109C7B7E23BC5E2E87A
3.153 +CA8E019203952A4892544E1AD3D4EDD22971611358AB230E9A2ABDF00A288501
3.154 +A01B67C42B33F6B78C39562DB50F4663B922D9BE0D8A150311AE44B83C1F129F
3.155 +07337323E9A23211EE58E16043E127C6F9574019179F5635648A011266677B56
3.156 +B5D0201A4E1470B952A1579B57AB2329CD4C615395023C653F784D36B5EE3672
3.157 +10D191F29EA508CE84763CA4CE7C2C5229E38E241255A5CABCD6C7CBAED901A2
3.158 +CA53B5E24111921CDDF83578D33D463D70EDACA0E470D8F592303FB6BFD68B4D
3.159 +3F3BE2D7C5EC8BBF10C90111A33E205F2649B56E8443F6FAA6C721C66575AE12
3.160 +D4C40F1F46CF9E9DA675AB5D5840D938780CD9E4AD6736ECBEB6A4397613586F
3.161 +849B51048AC5F9405E03E14540A5E5582F61CDCDB57EDDF95A8C6705F433EE16
3.162 +648F098C03DED8A2AD94AE3DE202D629B9422ABB031318D48F2C85F9DBFA17BE
3.163 +84708AA3B6C9F81F4508F7A5CB7B6646AB8722ECF817877B77D473F577556DAA
3.164 +2BA0ABACFCF5DEA7498C47328E873019A956FBB250FD9D8885D21D368FA70CBD
3.165 +2709D2DA44EE7A9869963EAB48789541906DE49FAE785ECE1F18A22C7E7ED204
3.166 +9768896B78E9EB7A2BD6EEC1B26083940656ECD689D92942CC8AF05CBF82AED0
3.167 +B45A7DF4DD7AA6526FB597322560B9ED3087A65B5EEF1371C328A021411BFE3B
3.168 +D9B5088B2F1AAE381FFED52D2D1E02CD0DA78683E3B06171CBE94BE9760005D7
3.169 +135893D7CC2DB097F6AC664D9594CF1C650F84DA80D2EDE04802DBA33CE3DAFE
3.170 +EB7A37E8AEFA4FDA6252FF21E8673DD98E67124D5DBC7BACF361E57077B71939
3.171 +C1D1FB923E4E35C075CD1BCBE0E80DAEA1320D55B43EAB45D9B26C366B278782
3.172 +7519FDC482D98839BF0DF2E7C3A56A1C1A3FC0E57A75CA414F6536C1FE8EB7A0
3.173 +4ADFEE3BEDA0F53BE8CF5F64230784A797133E8CD46BCCB3BF38BCE38A73CCE2
3.174 +9E073ADE792F7128231DDD1F63E6156ADB2609C200837C2E8A2D93D2A7BC9171
3.175 +050C709A71E44E32B1B03C92EB5CF1D3BAB1C38E027DC4ED9AED633D98CD7486
3.176 +3F773ACF8AE332631CF2ABE6D606607593FE862ADE31803964E3F4DC3CE3A271
3.177 +C76BDD95C87CDB3B87BC26FC7A16D567EEC62E6FF0D471B4853DB8A94D4CACF8
3.178 +843824F818083F10E88D52FC4253E8203292CB40F1414AE7E51DD7347007C342
3.179 +CD70E8E9F2D2A13D71213B841DDEAAB208AD9EA644591C15DEB084165F9DF24B
3.180 +B91D3BBEEC2E34E38EF16A0C3F00700A7BDCBBFED2EC0D09601AD6538288DB50
3.181 +3478B051B5E16B604A0341FE621A58718D960D699D3FAD284310DCF54EB13175
3.182 +19A75A539EE98E804AEA24689D3540F0F12951A3C01FACCE9A7BAF4D0DAFA946
3.183 +FF65A4D2A4C39969607272C6886F44E90ABE27CA3A1F12A29D9B32E60E8E34F0
3.184 +17C5FE43D0E69A99A922D98909B2BBCD145E59A5E7F5426B3988F73B09A525F6
3.185 +8BD4915663C1301323180E760BE81CB874B020FDA3AE63340E4261E4F3E4949B
3.186 +CC0966BDC4426190BE9F5D77F76A72AD925662E5FE1CEF9CCAB68F0BD33DA003
3.187 +F11EB91AC4502FBD6AE48DA0F9D07C35B96B103E379B8A83A05FE728F1716194
3.188 +1F650F75BEBADB2E3810388F3E2DC7B19F1BA9E32925F2FD9F19F4E8701F3E4E
3.189 +4069125D7C401144740691E7A460021A47B1E27997FC1DDABEC5BD0EE0B20194
3.190 +2D579C7D6727AA124083242BDA46D8E116E2751C5F298851A62B60AEBE82A929
3.191 +9B9F2492BA35690D1EFD16215B8EF14E7A3803B93C28FA41D971B05B6AF3B593
3.192 +E74AD1E68A5FCE12A86E63B78BFEA87D3949FD164F12277A4688BE96356791CB
3.193 +8671C49365608F3EDECC109321AF92B4C29CAF073DA3A7D73E913D0D83FAC5EB
3.194 +BD884D4C686056404DAAAD6F82F94F803FA1FB0DD8908D1DF08FB87A8BB83027
3.195 +04DE0CBB1C6FEB6B517FBD7CF065120079E608CE41893C2BC96A347826CCDFD5
3.196 +C69E161217F2127A59F1A6F22037641613F191F22D5B4CDCBCC2EE5615623404
3.197 +ABA7BE6C5FE475481615B2AC1A2412E54688DD21E44CC9AF5F16E634AFCA389C
3.198 +4D740B7B51BB141BFAD1080E7C726C1606A28ED492E6BDE9F800EFACD1513909
3.199 +84E98CEB6A0B7A2A6F3E1D1DCC3B2552795E0932673E59ECC56DDD37A1D52BA6
3.200 +C3F0E905978AB568941A163F4CE3AAB5C5B16F86016EC47BA6F3F7AAAA77C3B6
3.201 +09C8C3ABDB6D514A76ECD37C37AA88B5860630B3406B494F7725975596F84777
3.202 +D9CF48686EC9C5DBCC1D78513F591C7C10AB9D153B3D41426B7BF668B0D04503
3.203 +56BCB686258462C1DC61095724B9F3312316262FD7C1AEC6E54DE7E5A7BD8EFF
3.204 +035299B8FD8A4A7B0F51404F4A760F4D8B4C0FB7A32FA4B2383AB6E9C78FDEDB
3.205 +FE6A5788D38A6701B123630C2A6D820A684166FBBC83DB17069494FBD411B333
3.206 +CB37E2491C5BD035A33867A6D3A3D420CC31ACF43AA07182CAAE67E40EC63663
3.207 +B678F71D4C6E0EC3A0AAF904CD3AA66E0DE5E3CDE049E94249B39A1C06E3CE9A
3.208 +F974B2484BB2CDA14282B9511E505B3C89F9C802218AE40D1A7541335C5736DD
3.209 +CD565D4B9F4CC78F3A393737EDB4FBD0DA299E21CCFEBA5478EEF013F0552A8B
3.210 +0BB11FF46CCDB784E8BDCF730A16363E66572049E42C695886EAB42A9AD9094C
3.211 +B635DF4B5B9BD9B9AE8455DFA3EEFC77653190F9A8B1E93B7281C2A21EA7DDA9
3.212 +33484745BDF7E3DD63C7AC66C286C9A5A698A5E4D7A91710B7FF943FB23609B6
3.213 +4B442F83CB795788FAB5E9CF3F75D5487DA26170E4561C7941C910B088C3B86D
3.214 +F844B0F340CF82786A3FCF347048463EBD2006281A816627065DDA6CD4D3AC5E
3.215 +2024BC96C7D896381BBB567951E7A1F29D4E95351298B000D29E5F3D0448CB5A
3.216 +CFDAE1BADE9403B90371C3A07D208948AFA022A69C519434B6813086ADF518D5
3.217 +88E0B92072A44BA1B3EBB630A13B7AB90992E85B6D67361C8D96F3E0D826FF37
3.218 +17B67E4B1EB7BADFD98D7F4FD17BECE740ADF13C141EBF0A91CB105DABB32FE0
3.219 +55086D56A0D358841D15FD349E6B95512E4EDF4C430216FF85C2ABE995E4B40A
3.220 +A6044CC8820AD885C07E052B3F91C2E9A1D163BFFD210F7BE95B923E2500DB50
3.221 +2075106DB541C267BD450B25B670CE80BCD068D4DBFF2D82634175B61FBD3BC3
3.222 +406131F44C7D6F18D375D1F2270829DDF29DC14DBB58A30AC193245D18DE91F8
3.223 +AB88AB548D8138605BB5A50073295534E314366E26665AE70482B890E4101D6B
3.224 +60E4F3B37ABCA1346DAAE8FDB8DD9C832EFF3E73BA470E2BACE7B8515CB43388
3.225 +C27AF99FF9322175CF8D4947E6B3846AFF5163E972156847F58A66660EC8A3A6
3.226 +5FB47C9F637B4CBB4C73B6A080B0CF6FD1E9665E92032540570FFCC747C67C50
3.227 +822811AADC404BC7ECD1673E8AA6C3A2F1D82F39430B58C29145E2F1B679C46E
3.228 +94EDC711883F1E4EA84117A54757E8895A40401A26E1437B39A2F65CAADD6E02
3.229 +D71FA8AF7453668DC613F326A3344F74AD7AC67569AF399385500ABDA5EDD3BA
3.230 +343CC5EDD4B558467626850E752B9959FEF1454E53E7A3DCBC2255AD8F6AB4FE
3.231 +894455118A61C58840CB68A925ACCAD75CEACE863D806916228F0614191A1CD5
3.232 +DC9BAE256018615AA3725834519449B0A88B4F396654E74099C007930ADB1327
3.233 +DD119BF799FE3B0B223E1EDA04FE2DA7A1C879143E1C33B6C6344F4BA033AD6F
3.234 +8E88C33DEF1977796B454BAB2494C930F492A518E8198C708A75FFEF8C49C324
3.235 +A718AB59B889DED521229E741FFE53F98EBE88B0405AD523254FD3FA4BBE96DA
3.236 +DA1C27C1C979A0DD4E61C3B1F4C4DE01E42F1C4435EECFC02D97994BC8AF5270
3.237 +E7CB1458D76ED0229C5FFB4A23B8716018F9050970895D51722CDE8F2EA3D947
3.238 +DFF374D84915D5C5D16463A6FFCD079D1ED416C4347BF831FF0C4ADFB61295DC
3.239 +4D5785BB0852BF472CFC97EC174491CAF961AB90629F055E75DAA6D9898E8653
3.240 +5BCF379816CAE46FEA62E7BE8E9B953466E51828172C4DBD0E1BBAD1CE28B5B1
3.241 +02B3E36403BE80B49A47446A6677FCED438F01D60EB10F478C89528FA337D0D8
3.242 +88D3FC123C076507ACDAF783A9A6E24ED73BF24B6E0F11C13E532DE5F70B15A0
3.243 +657F5ED27D204449A841ED19E01432CFFE928E921321113780D036D34F2797DE
3.244 +D4459CFD15BB117B5C9745EF3CD2B296D91FAD48C80B136D94476967E255F808
3.245 +AD2B5D522ADEC64176833756510391815A1D4A8DA1D0AEE7CAD36A1D161889F2
3.246 +3347D5B6BC503300FDDD48F594F391D5FB42C42113C538E707C16EE24A3F375E
3.247 +7C506E8F49CE50FF9DEF3B4A4C1BEB3848EAA3477349833BA22D2A9012287D8B
3.248 +A8C4CB4307A1188ACC0E6E9338E1559BE5FAFF381BD82A6C71C267409468B3C0
3.249 +2C1A29F4281D565836EAE57F680490FEA4A952FF64C8CD11C377C294DCD1EC25
3.250 +CEFB2B6DCE959D0208F85B6E32E9B44FD455F9B134A5306D95EA29F37BB8B86D
3.251 +9E592159338E1293F449380E13C21AE42E692F6C00B521F7AB2F32545952358F
3.252 +0D39246DE215D0A7EE67F377E81F9E65B25658B7FD97FAF98C7EA9161530404B
3.253 +62B9AB7A91C863095D5433BB06F9A29488DA84D58A1394AD7878BB27E3CF4AF1
3.254 +BC29DC64F319758518AB652F9E8BCA586D3D2021CA860F84DC0A2F61A93B6B44
3.255 +F08A7F7C5F36FEE9F5D450D19F72C09580DDE2B3747D8A1054981BAEF31D6C42
3.256 +040D7D5F37DE6DE019849E7C7754DD27E9511F9A9AFA4FB727695444F739448F
3.257 +3D2021
3.258 +0000000000000000000000000000000000000000000000000000000000000000
3.259 +0000000000000000000000000000000000000000000000000000000000000000
3.260 +0000000000000000000000000000000000000000000000000000000000000000
3.261 +0000000000000000000000000000000000000000000000000000000000000000
3.262 +0000000000000000000000000000000000000000000000000000000000000000
3.263 +0000000000000000000000000000000000000000000000000000000000000000
3.264 +0000000000000000000000000000000000000000000000000000000000000000
3.265 +0000000000000000000000000000000000000000000000000000000000000000
3.266 +cleartomark
3.267 +{restore}if
3.268 +%%EndFont
3.269 TeXDict begin 39158280 55380996 1000 600 600 (Protokoll.dvi)
3.270 -@start /Fa 87[33 45[44 1[50 2[55 33 39 44 1[55 50 55
3.271 -83 28 55 33 28 55 50 33 44 55 44 55 50 10[72 1[66 55
3.272 -2[61 1[72 4[39 3[66 2[66 72 11[50 50 50 50 50 2[25 33
3.273 -45[{TeXBase1Encoding ReEncodeFont}39 99.6264 /Times-Bold
3.274 -rf /Fb 32[42 54[28 45[37 42 42 60 42 42 23 32 28 42 42
3.275 -42 42 65 23 42 23 23 42 42 28 37 42 37 42 37 6[51 2[78
3.276 -60 60 51 46 55 1[46 60 60 74 51 60 32 28 60 60 46 51
3.277 -60 55 55 60 6[23 7[42 42 1[23 21 28 21 2[28 28 28 36[46
3.278 -2[{TeXBase1Encoding ReEncodeFont}62 83.022 /Times-Roman
3.279 -rf /Fc 87[40 45[53 4[66 40 47 53 1[66 60 66 100 33 66
3.280 -40 33 66 60 40 53 66 53 66 60 6[80 6[66 86 1[73 2[113
3.281 -3[47 6[80 86 6[40 4[60 60 60 60 60 3[40 45[{
3.282 -TeXBase1Encoding ReEncodeFont}37 119.552 /Times-Bold
3.283 -rf /Fd 87[33 45[44 2[72 1[50 28 39 33 2[50 50 78 28 50
3.284 +@start /Fa 240[42 15[{}1 83.022 /CMSY10 rf /Fb 87[33
3.285 +45[44 1[50 2[55 33 39 44 1[55 50 55 83 28 55 33 28 55
3.286 +50 33 44 55 44 55 50 10[72 1[66 55 2[61 1[72 4[39 3[66
3.287 +2[66 72 6[33 50 50 50 1[50 50 50 50 50 50 1[25 33 45[{
3.288 +TeXBase1Encoding ReEncodeFont}44 99.6264 /Times-Bold
3.289 +rf /Fc 32[42 54[28 19[37 25[37 42 42 60 42 42 23 32 28
3.290 +42 42 42 42 65 23 42 23 23 42 42 28 37 42 37 42 37 6[51
3.291 +1[60 78 60 60 51 46 55 60 46 1[60 74 51 60 32 28 60 60
3.292 +46 51 60 55 55 60 5[23 23 42 42 42 42 42 42 42 42 42
3.293 +42 23 21 28 21 2[28 28 28 36[46 2[{TeXBase1Encoding ReEncodeFont}73
3.294 +83.022 /Times-Roman rf /Fd 87[40 45[53 4[66 40 47 53
3.295 +1[66 60 66 100 33 66 40 33 66 60 40 53 66 53 66 60 6[80
3.296 +6[66 86 1[73 2[113 3[47 6[80 86 6[40 4[60 60 60 60 60
3.297 +3[40 45[{TeXBase1Encoding ReEncodeFont}37 119.552 /Times-Bold
3.298 +rf /Fe 87[33 45[44 2[72 1[50 28 39 33 2[50 50 78 28 50
3.299 1[28 50 50 33 44 1[44 50 44 11[72 61 55 5[89 3[33 1[72
3.300 4[66 15[50 50 50 3[25 44[{TeXBase1Encoding ReEncodeFont}31
3.301 -99.6264 /Times-Roman rf /Fe 87[48 49[72 72 40 56 48 1[72
3.302 +99.6264 /Times-Roman rf /Ff 87[48 49[72 72 40 56 48 1[72
3.303 72 72 112 1[72 40 40 72 1[48 64 72 64 72 64 11[104 88
3.304 80 2[80 2[128 3[48 5[96 21[48 45[{TeXBase1Encoding ReEncodeFont}28
3.305 143.462 /Times-Roman rf end
3.306 @@ -255,15 +496,15 @@
3.307 end
3.308 %%EndSetup
3.309 %%Page: 1 1
3.310 -TeXDict begin 1 0 bop 526 739 a Fe(Userinterf)o(aces)32
3.311 +TeXDict begin 1 0 bop 526 739 a Ff(Userinterf)o(aces)32
3.312 b(f)1449 738 y(\250)1437 739 y(ur)j(Computer)f(Theorem)g(Pro)n(v)n(er)
3.313 775 922 y(Machbark)o(eits-Studie)d(im)k(Isac-Projekt)1561
3.314 -1162 y Fd(Marco)25 b(Ste)o(ger)1326 1279 y(Bachelorarbeit)g(T)-7
3.315 +1162 y Fe(Marco)25 b(Ste)o(ger)1326 1279 y(Bachelorarbeit)g(T)-7
3.316 b(elematik)1121 1395 y(am)24 b(Institut)g(f)8 b(\250)-41
3.317 b(ur)25 b(Softw)o(aretechnologie)1654 1511 y(TU)g(Graz)1538
3.318 -1705 y(March)g(1,)g(2011)330 2064 y Fc(1)119 b(Zur)31
3.319 +1705 y(March)g(2,)g(2011)330 2064 y Fd(1)119 b(Zur)31
3.320 b(A)-6 b(ufgabenstellung)31 b(der)g(Bachelorarbeit)330
3.321 -2250 y Fb(Computer)17 b(Theorem)f(Pro)o(v)o(er)h(\(CTP\))h(sind)g(bis)h
3.322 +2250 y Fc(Computer)17 b(Theorem)f(Pro)o(v)o(er)h(\(CTP\))h(sind)g(bis)h
3.323 (dato)f(in)g(H)5 b(\250)-33 b(anden)17 b(eines)h(relati)n(v)g(kleinen)f
3.324 (Kreises)i(v)n(on)330 2349 y(Experten,)f(v)n(on)h(denen)f(der)h
3.325 (Gro\337teil)g(wiederum)f(im)i(akademischen)e(Bereich)h(arbeitet)g(und)
3.326 @@ -306,8 +547,8 @@
3.327 y(auf)32 b(jEdit)h(und)e(Isabelle)i(aufgesetzt)e(werden.)61
3.328 b(Die)33 b(Bachelorarbeit)e(liefert)i(die)f(Machbark)o(eits-)330
3.329 4142 y(Studie)20 b(f)7 b(\250)-35 b(ur)20 b(diesen)f(Schritt.)330
3.330 -4422 y Fc(2)119 b(Ist-Zustand)29 b(zu)i(Pr)n(ojektbeginn)330
3.331 -4608 y Fb(ISA)m(C)19 b(wird)e(als)i(Eclipse-Projekt)e(entwick)o(elt,)h
3.332 +4422 y Fd(2)119 b(Ist-Zustand)29 b(zu)i(Pr)n(ojektbeginn)330
3.333 +4608 y Fc(ISA)m(C)19 b(wird)e(als)i(Eclipse-Projekt)e(entwick)o(elt,)h
3.334 (das)g(das)h(Ja)n(v)n(aSwing-Frontend)c(und)i(auch)g(die)i(SML-)330
3.335 4707 y(Mathematik-Engine)12 b(\(samt)j(einer)g(alten)g(Isabelle-V)-9
3.336 b(ersion\))13 b(umf)o(asst.)23 b(Isabelles)15 b(k)o(ommende)e
3.337 @@ -318,32 +559,206 @@
3.338 (Entwicklungs-Umgeb)n(ung.)455 5006 y(So)n(w)o(ohl)e(zu)i(jEdit)f(als)h
3.339 (auch)f(zu)g(Scala)h(und)e(NetBeans)i(bestehen)e(k)o(eine)h(Erf)o
3.340 (ahrungen)d(im)k(ISA)m(C-)330 5106 y(Projekt.)330 5385
3.341 -y Fc(3)119 b(Planung:)38 b(Soll-Zustand)31 b(am)e(Pr)n(ojektende)330
3.342 -5571 y Fb(ISA)m(C)24 b(ist)g(in)g(die)g(Isabelle-Entwicklung)c(inte)o
3.343 +y Fd(3)119 b(Planung:)38 b(Soll-Zustand)31 b(am)e(Pr)n(ojektende)330
3.344 +5571 y Fc(ISA)m(C)24 b(ist)g(in)g(die)g(Isabelle-Entwicklung)c(inte)o
3.345 (griert,)j(die)g(ISA)m(C-Entwicklung)e(l)5 b(\250)-33
3.346 b(auft)24 b(in)f(einem)g(up-)330 5670 y(datebaren)c(Repository)g(v)n
3.347 (on)h(Isabelle.)25 b(F)7 b(\250)-35 b(ur)21 b(das)f(in)h(Entwicklung)d
3.348 (be\002ndliche)h(jEdit-Frontend)f(v)n(on)1809 5919 y(1)p
3.349 eop end
3.350 %%Page: 2 2
3.351 -TeXDict begin 2 1 bop 330 390 a Fb(Isabelle)26 b(ist)i(ein)f
3.352 +TeXDict begin 2 1 bop 330 390 a Fc(Isabelle)26 b(ist)i(ein)f
3.353 (NetBeans-Projekt)e(aufgesetzt.)43 b(W)-7 b(esentliche)27
3.354 b(V)-11 b(orarbeiten)25 b(haben)h(die)g(Heraus-)330 490
3.355 y(forderungen)21 b(gekl)5 b(\250)-33 b(art,)26 b(die)f(sich)h(aus)f
3.356 (der)g(Zielsetzung)f(er)o(geben:)33 b(Backs)26 b(')-5
3.357 b(structured)24 b(deri)n(v)n(ations')337 589 y(\250)-35
3.358 b(uber)19 b(das)i(neue)e(jEdit-GUI)h(eingeben)e(und)h(v)n(on)h
3.359 -(Isabelle)g(check)o(en)f(lassen.)330 870 y Fc(4)119 b(Milestones)30
3.360 -b(und)h(Arbeitspr)n(otok)n(olle)330 1072 y Fa(4.1)99
3.361 -b(Inhaltliche)26 b(V)-10 b(oraussetzungen)26 b(erarbeitet)330
3.362 -1227 y Fb(T)o(ODO)330 1465 y Fa(4.2)99 b(T)-9 b(echnische)27
3.363 -b(V)-10 b(oraussetzungen)26 b(her)o(gestellt)330 1621
3.364 -y Fb(T)o(ODO)330 1858 y Fa(4.3)99 b(NetBeans-Pr)n(ojekt)27
3.365 -b(aufgesetzt)330 2031 y(4.4)99 b(Experimentelle)27 b(P)o(arser)e
3.366 -(implementiert)330 2203 y(4.5)99 b(Pr)667 2202 y(\250)659
3.367 -2203 y(asentation)25 b(der)h(Arbeit)g(im)e(IST)-9 b(-Seminar)330
3.368 -2408 y Fc(5)119 b(Zusammenfassung)29 b(und)i(R)1824 2407
3.369 -y(\250)1811 2408 y(uckblick)1809 5919 y Fb(2)p eop end
3.370 +(Isabelle)g(check)o(en)f(lassen.)330 870 y Fd(4)119 b(Milestones)30
3.371 +b(und)h(Arbeitspr)n(otok)n(olle)330 1072 y Fb(4.1)99
3.372 +b(Inhaltliche)26 b(V)-10 b(oraussetzungen)26 b(erarbeitet:)33
3.373 +b(am)24 b(27.09.2010)455 1227 y Fa(\017)41 b Fc(K)n(enntnis)19
3.374 +b(der)h(Grundlagen)d(und)j(Anwendung)d(v)n(on)j(CTP:)h(am)f(03.08.2010)
3.375 +455 1394 y Fa(\017)41 b Fc(Charakteristika)19 b(der)g(Programmsprache)e
3.376 +(Scala:)26 b(27.09.2010)455 1560 y Fa(\017)41 b Fc(Scala)20
3.377 +b(Actors:)25 b(am)20 b(12.08.2010)p 330 1655 3134 4 v
3.378 +328 1755 4 100 v 380 1725 a(Datum)p 900 1755 V 345 w(T)5
3.379 +b(\250)-33 b(atigk)o(eit)p 2890 1755 V 1689 w(Einheiten)p
3.380 +3462 1755 V 330 1758 3134 4 v 328 1958 4 200 v 380 1828
3.381 +a(12.07.2010)p 900 1958 V 194 w(Meeting:)29 b(erste)22
3.382 +b(Besprechung)f(und)g(Erklrungen)e(zu)k(Isabelle,)952
3.383 +1928 y(Isac)d(und)g(CTPs)p 2890 1958 V 2941 1828 a(2)p
3.384 +3462 1958 V 330 1961 3134 4 v 328 2061 4 100 v 380 2031
3.385 +a(15.07.2010)p 900 2061 V 194 w(Recherche)f(ber)h(Isabelle)g(und)f
3.386 +(CTPs)p 2890 2061 V 883 w(3)p 3462 2061 V 330 2064 3134
3.387 +4 v 328 2263 4 200 v 380 2134 a(20.07.2010)p 900 2263
3.388 +V 194 w(Meeting:)33 b(Besprechen)23 b(der)h(grundstzlichen)d(V)-11
3.389 +b(or)o(gangsweise)952 2233 y(und)19 b(Ziele)p 2890 2263
3.390 +V 2941 2134 a(1)p 3462 2263 V 330 2266 3134 4 v 328 2466
3.391 +4 200 v 380 2336 a(23.07.2010)p 900 2466 V 194 w(Isabelle:)25
3.392 +b(Ziele,)20 b(T)-6 b(echnik)o(en)18 b(\(ML\))h(und)g(Zusammenhnge)e
3.393 +(mit)952 2436 y(Isac)j(abklren)p 2890 2466 V 2941 2336
3.394 +a(1)p 3462 2466 V 330 2469 3134 4 v 328 2668 4 200 v
3.395 +380 2539 a(30.07.2010)p 900 2668 V 194 w(Ende)31 b(der)h
3.396 +(Einarbeitungstage:)47 b(weitere)33 b(V)-11 b(or)o(gensweise)31
3.397 +b(ber)952 2638 y(Backs)21 b(')-5 b(structured)18 b(deri)n(v)n(ations';)
3.398 +h(Be)o(grif)n(fserklrung)p 2890 2668 V 2941 2539 a(3)p
3.399 +3462 2668 V 330 2672 3134 4 v 328 2771 4 100 v 380 2741
3.400 +a(01.08.2010)p 900 2771 V 194 w(Recherche:)24 b(Buch)c(fr)g(Scala)p
3.401 +2890 2771 V 1138 w(2)p 3462 2771 V 330 2775 3134 4 v
3.402 +328 2874 4 100 v 380 2844 a(03.08.2010)p 900 2874 V 194
3.403 +w(Isabelle)g(bestehende)e(T)-6 b(echnologie)18 b(studieren)p
3.404 +2890 2874 V 585 w(4)p 3462 2874 V 330 2877 3134 4 v 328
3.405 +3077 4 200 v 380 2947 a(05.08.2010)p 900 3077 V 194 w(Einarbeiten)46
3.406 +b(in)h(Scala:)81 b(Unterschiede)46 b(zu)h(Ja)n(v)n(a)h(indenti-)952
3.407 +3047 y(\002zieren)p 2890 3077 V 2941 2947 a(1)p 3462
3.408 +3077 V 330 3080 3134 4 v 328 3279 4 200 v 380 3150 a(06.08.2010)p
3.409 +900 3279 V 194 w(Einarbeiten)e(in)h(Scala:)81 b(Unterschiede)46
3.410 +b(zu)h(Ja)n(v)n(a)h(indenti-)952 3249 y(\002zieren,)19
3.411 +b(erste)i(Beispiel\002les)p 2890 3279 V 2941 3150 a(4)p
3.412 +3462 3279 V 330 3283 3134 4 v 328 3382 4 100 v 380 3352
3.413 +a(08.08.2010)p 900 3382 V 194 w(Einarbeiten)d(in)j(Scala:)k
3.414 +(funktionale)18 b(Seite)j(v)n(on)f(Scala)p 2890 3382
3.415 +V 362 w(2)p 3462 3382 V 330 3386 3134 4 v 328 3485 4
3.416 +100 v 380 3455 a(09.08.2010)p 900 3485 V 194 w(Einarbeiten)e(in)j
3.417 +(Scala:)k(T)-6 b(est\002les)22 b(mit)e(Scala-Swing)p
3.418 +2890 3485 V 423 w(5)p 3462 3485 V 330 3488 3134 4 v 328
3.419 +3588 4 100 v 380 3558 a(12.08.2010)p 900 3588 V 194 w(Studieren)f(v)n
3.420 +(on)g(P)o(apers)h(zu)g(Scala)h(Actors)p 2890 3588 V 744
3.421 +w(3)p 3462 3588 V 330 3591 3134 4 v 328 3691 4 100 v
3.422 +380 3661 a(24.09.2010)p 900 3691 V 194 w(Scala:)26 b(Arbeiten)19
3.423 +b(mit)h(Klassen)h(und)e(Schnittstellen)p 2890 3691 V
3.424 +436 w(3)p 3462 3691 V 330 3694 3134 4 v 328 3794 4 100
3.425 +v 380 3764 a(25.09.2010)p 900 3794 V 194 w(Scala:)26
3.426 +b(Experimente)18 b(mit)i(Ja)n(v)n(a)h(in)f(Scala-Source)p
3.427 +2890 3794 V 494 w(6)p 3462 3794 V 330 3797 3134 4 v 328
3.428 +3897 4 100 v 380 3867 a(27.09.2010)p 900 3897 V 194 w(Scala:)26
3.429 +b(T)-6 b(est\002les)21 b(zu)f(\224Funktional)e(vs)j(Imperati)n(v\224)p
3.430 +2890 3897 V 493 w(4)p 3462 3897 V 330 3900 3134 4 v 328
3.431 +4000 4 100 v 900 4000 V 952 3970 a(Anzahl)e(der)h(Einheiten)p
3.432 +2890 4000 V 1282 w(112)p 3462 4000 V 330 4003 3134 4
3.433 +v 330 4202 a Fb(4.2)99 b(T)-9 b(echnische)27 b(V)-10
3.434 +b(oraussetzungen)26 b(her)o(gestellt:)32 b(am)25 b(02.08.2010)455
3.435 +4357 y Fa(\017)41 b Fc(Isabelle)20 b(installiert,)g(Filestruktur)f
3.436 +(bekannt:)24 b(am)c(02.08.2010)455 4523 y Fa(\017)41
3.437 +b Fc(Scala)20 b(in)g(NetBeans)h(eingeb)n(unden:)h(am)f(22.07.2010)455
3.438 +4689 y Fa(\017)41 b Fc(Mercurial)19 b(installiert)h(und)f(einrichten)g
3.439 +(des)i(Repositories:)j(19.07.2010)1809 5919 y(2)p eop
3.440 +end
3.441 +%%Page: 3 3
3.442 +TeXDict begin 3 2 bop 330 311 3134 4 v 328 410 4 100
3.443 +v 380 380 a Fc(Datum)p 900 410 V 345 w(T)5 b(\250)-33
3.444 +b(atigk)o(eit)p 2890 410 V 1689 w(Einheiten)p 3462 410
3.445 +V 330 413 3134 4 v 328 513 4 100 v 380 483 a(19.07.2010)p
3.446 +900 513 V 194 w(Be)o(ginn)19 b(der)h(Installationsarbeiten:)j(Repo)d
3.447 +(klonen)f(und)g(testen)p 2890 513 V 99 w(6)p 3462 513
3.448 +V 330 516 3134 4 v 328 616 4 100 v 380 586 a(20.07.2010)p
3.449 +900 616 V 194 w(Installationsarbeiten,)f(Einarbeiten)g(in)j
3.450 +(Filestruktur)p 2890 616 V 396 w(7)p 3462 616 V 330 619
3.451 +3134 4 v 328 719 4 100 v 380 689 a(21.07.2010)p 900 719
3.452 +V 194 w(Einarbeiten)d(in)j(Filestruktur)p 2890 719 V
3.453 +1111 w(6)p 3462 719 V 330 722 3134 4 v 328 922 4 200
3.454 +v 380 792 a(22.07.2010)p 900 922 V 194 w(V)-11 b(orbereitungen:)41
3.455 +b(NetBeans,)31 b(JDK)g(und)d(Scala)i(installieren.)952
3.456 +892 y(Scala)20 b(in)h(NetBeans)f(inte)o(grieren)p 2890
3.457 +922 V 2941 792 a(8)p 3462 922 V 330 925 3134 4 v 328
3.458 +1024 4 100 v 380 995 a(23.07.2010)p 900 1024 V 194 w
3.459 +(Isabelle-jEdit-Plugin)d(mittels)k(NetBeans)g(ausfhren:)i(testen)p
3.460 +2890 1024 V 158 w(5)p 3462 1024 V 330 1028 3134 4 v 328
3.461 +1127 4 100 v 380 1098 a(27.07.2010)p 900 1127 V 194 w
3.462 +(Isabelle-jEdit-Plugin:)g(nderungen)17 b(an)j(der)g(Projektstruktur)p
3.463 +2890 1127 V 150 w(7)p 3462 1127 V 330 1131 3134 4 v 328
3.464 +1230 4 100 v 380 1200 a(28.07.2010)p 900 1230 V 194 w(Experimente)e
3.465 +(mit)i(Isabelle-jEdit-Plugin)p 2890 1230 V 718 w(6)p
3.466 +3462 1230 V 330 1234 3134 4 v 328 1333 4 100 v 380 1303
3.467 +a(29.07.2010)p 900 1333 V 194 w(Identi\002kations)e(der)i(P)o
3.468 +(arse-Einstie)o(gsstelle)p 2890 1333 V 676 w(5)p 3462
3.469 +1333 V 330 1337 3134 4 v 328 1536 4 200 v 380 1406 a(30.07.2010)p
3.470 +900 1536 V 194 w(Experimente)j(mit)i(Isabelle-jEdit-Plugin,)e
3.471 +(Besprechung)g(ber)952 1506 y(Erf)o(ahrungen)17 b(mit)j(Filestruktur)p
3.472 +2890 1536 V 2941 1406 a(4)p 3462 1536 V 330 1539 3134
3.473 +4 v 328 1738 4 200 v 380 1609 a(02.08.2010)p 900 1738
3.474 +V 194 w(Installationen)g(und)h(einrichten)f(des)i(Repos)g(auf)f(meinen)
3.475 +g(Lap-)952 1709 y(top)p 2890 1738 V 2941 1609 a(6)p 3462
3.476 +1738 V 330 1742 3134 4 v 330 1758 V 328 1858 4 100 v
3.477 +900 1858 V 952 1828 a(Anzahl)e(der)h(Einheiten)p 2890
3.478 +1858 V 1282 w(32)p 3462 1858 V 330 1861 3134 4 v 330
3.479 +2060 a Fb(4.3)99 b(NetBeans-Pr)n(ojekt)27 b(aufgesetzt)455
3.480 +2215 y Fa(\017)41 b Fc(Grundle)o(gende)16 b(Projektstruktur)i(f)7
3.481 +b(\250)-35 b(ur)20 b(ISA)m(C)g(her)o(gestellt:)25 b(am)20
3.482 +b(02.08.2010)455 2381 y Fa(\017)41 b Fc(jEdit-Plugin:)23
3.483 +b(XML-Files)e(fr)f(ISA)m(C)g(v)n(orbereitet:)k(am)c(22.07.2010)455
3.484 +2547 y Fa(\017)41 b Fc(jEdit-Plugin:)23 b(Source)d(\002les)h
3.485 +(geschrieben:)i(19.07.2010)p 330 2660 V 328 2760 4 100
3.486 +v 380 2730 a(Datum)p 900 2760 V 345 w(T)5 b(\250)-33
3.487 +b(atigk)o(eit)p 2890 2760 V 1689 w(Einheiten)p 3462 2760
3.488 +V 330 2763 3134 4 v 328 2863 4 100 v 380 2833 a(10.08.2010)p
3.489 +900 2863 V 194 w(Projektstruktur)18 b(anle)o(gen,)g(b)n(uild.xml)h
3.490 +(anpassen)p 2890 2863 V 531 w(7)p 3462 2863 V 330 2866
3.491 +3134 4 v 328 2966 4 100 v 380 2936 a(11.08.2010)p 900
3.492 +2966 V 194 w(jEdit-Plugin-Struktur)d(studieren:)25 b(Ho)n(wto)19
3.493 +b(durcharbeiten)p 2890 2966 V 205 w(5)p 3462 2966 V 330
3.494 +2969 3134 4 v 328 3069 4 100 v 380 3039 a(21.08.2010)p
3.495 +900 3069 V 194 w(bestehende)g(jEdit-Plugins)g(\(Ja)n(v)n(a\))g
3.496 +(durcharbeiten)p 2890 3069 V 461 w(3)p 3462 3069 V 330
3.497 +3072 3134 4 v 328 3172 4 100 v 380 3142 a(22.08.2010)p
3.498 +900 3172 V 194 w(K)m(opieren)e(des)h(Isabelle-jEdit-Plugins,)f
3.499 +(Umarbeiten)g(fr)h(ISA)m(C)p 2890 3172 V 99 w(3)p 3462
3.500 +3172 V 330 3175 3134 4 v 328 3274 4 100 v 380 3245 a(24.08.2010)p
3.501 +900 3274 V 194 w(Umarbeiten)h(des)h(Isabelle-Plugins)f(fr)h(ISA)m(C)p
3.502 +2890 3274 V 627 w(6)p 3462 3274 V 330 3278 3134 4 v 328
3.503 +3477 4 200 v 380 3348 a(26.08.2010)p 900 3477 V 194 w(Problem)34
3.504 +b(mit)i(Isabelle-Umgeb)n(ungsv)n(ariable:)51 b(Suche)35
3.505 +b(nach)952 3447 y(Lsungen)p 2890 3477 V 2941 3348 a(3)p
3.506 +3462 3477 V 330 3480 3134 4 v 328 3680 4 200 v 380 3550
3.507 +a(28.08.2010)p 900 3680 V 194 w(Recherchen)21 b(zum)h(Umgeb)n(ungsv)n
3.508 +(ariable-Problem,)17 b(Arbeiten)952 3650 y(mit)j(den)g
3.509 +(Isabelle-Shell-Skripts)p 2890 3680 V 2941 3550 a(2)p
3.510 +3462 3680 V 330 3683 3134 4 v 328 3783 4 100 v 380 3753
3.511 +a(29.08.2010)p 900 3783 V 194 w(Experimente)e(mit)i(den)g(P)o(ath-V)-9
3.512 +b(arialbe)18 b(der)i(jvm)p 2890 3783 V 544 w(3)p 3462
3.513 +3783 V 330 3786 3134 4 v 328 3885 4 100 v 380 3856 a(30.08.2010)p
3.514 +900 3885 V 194 w(Isabelle-jEdit-Plugin)c(endlich)h(v)n(ollstndig)h
3.515 +(lauf)n(fhig)f(gebracht)p 2890 3885 V 97 w(4)p 3462 3885
3.516 +V 330 3889 3134 4 v 328 3988 4 100 v 380 3959 a(01.09.2010)p
3.517 +900 3988 V 194 w(Arbeiten)i(an)h(der)g(jEdit-ISA)m(C-Projektstruktur)p
3.518 +2890 3988 V 547 w(3)p 3462 3988 V 330 3992 3134 4 v 328
3.519 +4091 4 100 v 380 4061 a(04.09.2010)p 900 4091 V 194 w(Umarbeiten)f(des)
3.520 +h(Isabelle-Plugins)f(fr)h(ISA)m(C)p 2890 4091 V 627 w(5)p
3.521 +3462 4091 V 330 4095 3134 4 v 328 4194 4 100 v 380 4164
3.522 +a(20.09.2010)p 900 4194 V 194 w(Einrichten)f(des)h(Laptops)f(fr)h
3.523 +(Isabelle-Isac)p 2890 4194 V 706 w(4)p 3462 4194 V 330
3.524 +4198 3134 4 v 328 4397 4 200 v 380 4267 a(22.09.2010)p
3.525 +900 4397 V 194 w(Meeting:)27 b(F)o(ortschrittsbericht,)20
3.526 +b(kurze)h(Einfhrung)e(fr)i(Mitstre-)952 4367 y(iter)p
3.527 +2890 4397 V 2941 4267 a(3)p 3462 4397 V 330 4400 3134
3.528 +4 v 328 4699 4 299 v 380 4470 a(29.09.2010)p 900 4699
3.529 +V 194 w(Neue)28 b(V)-11 b(or)o(gehensweise:)39 b
3.530 +(QuickNotepad-Plugin\(QN\))23 b(wird)952 4570 y(in)33
3.531 +b(Scala)h(bersetzt)f(und)g(fr)g(ISA)m(C)h(entsprechend)d(angepasst:)952
3.532 +4669 y(Arbeit)20 b(an)g(den)g(XML-Files)p 2890 4699 V
3.533 +2941 4470 a(4)p 3462 4699 V 330 4702 3134 4 v 328 4802
3.534 +4 100 v 380 4772 a(30.09.2010)p 900 4802 V 194 w(QN:)h(Start)f(mit)h
3.535 +(bersetzten)e(der)h(Source\002les)p 2890 4802 V 662 w(5)p
3.536 +3462 4802 V 330 4805 3134 4 v 328 4905 4 100 v 380 4875
3.537 +a(02.10.2010)p 900 4905 V 194 w(QN:)h(bersetzten)e(der)h(Source\002les)
3.538 +p 2890 4905 V 971 w(6)p 3462 4905 V 330 4908 3134 4 v
3.539 +328 5008 4 100 v 380 4978 a(04.10.2010)p 900 5008 V 194
3.540 +w(QN:)h(bersetzten)e(der)h(Source\002les:)k(Problem)c(bei)g(Interf)o
3.541 +(ace)p 2890 5008 V 203 w(3)p 3462 5008 V 330 5011 3134
3.542 +4 v 328 5111 4 100 v 380 5081 a(05.10.2010)p 900 5111
3.543 +V 194 w(QN:)h(QN)f(v)n(ollstndig)g(in)g(Scala)g(bersetzt,)g(testen)p
3.544 +2890 5111 V 554 w(2)p 3462 5111 V 330 5114 3134 4 v 330
3.545 +5131 V 328 5230 4 100 v 900 5230 V 952 5201 a(Anzahl)f(der)h(Einheiten)
3.546 +p 2890 5230 V 1282 w(32)p 3462 5230 V 330 5234 3134 4
3.547 +v 1809 5919 a(3)p eop end
3.548 +%%Page: 4 4
3.549 +TeXDict begin 4 3 bop 330 390 a Fb(4.4)99 b(Experimentelle)27
3.550 +b(P)o(arser)e(implementiert)330 562 y(4.5)99 b(Pr)667
3.551 +561 y(\250)659 562 y(asentation)25 b(der)h(Arbeit)g(im)e(IST)-9
3.552 +b(-Seminar)330 768 y Fd(5)119 b(Zusammenfassung)29 b(und)i(R)1824
3.553 +767 y(\250)1811 768 y(uckblick)1809 5919 y Fc(4)p eop
3.554 +end
3.555 %%Trailer
3.556
3.557 userdict /end-hook known{end-hook}if
4.1 --- a/doc-src/isac/Protokoll_Steger_Marco/Protokoll.tex Thu Mar 10 12:45:58 2011 +0100
4.2 +++ b/doc-src/isac/Protokoll_Steger_Marco/Protokoll.tex Thu Mar 10 15:12:55 2011 +0100
4.3 @@ -45,21 +45,90 @@
4.4 %\newpage
4.5
4.6 \section{Milestones und Arbeitsprotokolle}
4.7 -\subsection{Inhaltliche Voraussetzungen erarbeitet}% am ..(*)...}
4.8 -TODO
4.9 -%\begin{itemize}
4.10 -%\item Kenntnis der Grundlagen und Anwendung von CTP
4.11 -%\item Charakteristika der Programmsprache Scala
4.12 -%\item Scala Actors
4.13 -%\end{itemize}
4.14 -\subsection{Technische Voraussetzungen hergestellt}% am ..(*)...}
4.15 -TODO
4.16 -%\begin{itemize}
4.17 -%\item Isabelle installiert, Filestruktur bekannt
4.18 -%\item Scala in NetBeans eingebunden
4.19 -%\item Mercurial installiert und einrichten des Repositories
4.20 -%\end{itemize}
4.21 +\subsection{Inhaltliche Voraussetzungen erarbeitet: am 27.09.2010}
4.22 +\begin{itemize}
4.23 +\item Kenntnis der Grundlagen und Anwendung von CTP: am 03.08.2010
4.24 +\item Charakteristika der Programmsprache Scala: 27.09.2010
4.25 +\item Scala Actors: am 12.08.2010
4.26 +\end{itemize}
4.27 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.28 +\hline
4.29 +Datum & T\"atigkeit & Einheiten \\ \hline
4.30 +12.07.2010 & Meeting: erste Besprechung und Erklärungen zu Isabelle, Isac und CTPs & 2 \\ \hline
4.31 +15.07.2010 & Recherche über Isabelle und CTPs & 3 \\ \hline
4.32 +20.07.2010 & Meeting: Besprechen der grundsätzlichen Vorgangsweise und Ziele & 1 \\ \hline
4.33 +23.07.2010 & Isabelle: Ziele, Techniken (ML) und Zusammenhänge mit Isac abklären & 1 \\ \hline
4.34 +30.07.2010 & Ende der Einarbeitungstage: weitere Vorgensweise über Backs 'structured derivations'; Begriffserklärung & 3 \\ \hline
4.35 +01.08.2010 & Recherche: Buch für Scala & 2 \\ \hline
4.36 +03.08.2010 & Isabelle bestehende Technologie studieren & 4 \\ \hline
4.37 +05.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren & 1 \\ \hline
4.38 +06.08.2010 & Einarbeiten in Scala: Unterschiede zu Java indentifizieren, erste Beispielfiles & 4 \\ \hline
4.39 +08.08.2010 & Einarbeiten in Scala: funktionale Seite von Scala & 2 \\ \hline
4.40 +09.08.2010 & Einarbeiten in Scala: Testfiles mit Scala-Swing & 5 \\ \hline
4.41 +12.08.2010 & Studieren von Papers zu Scala Actors & 3 \\ \hline
4.42 +24.09.2010 & Scala: Arbeiten mit Klassen und Schnittstellen & 3 \\ \hline
4.43 +25.09.2010 & Scala: Experimente mit Java in Scala-Source & 6 \\ \hline
4.44 +27.09.2010 & Scala: Testfiles zu "Funktional vs Imperativ" & 4 \\ \hline
4.45 + & Anzahl der Einheiten & 44 \\
4.46 +\hline
4.47 +\end{tabular}
4.48 +
4.49 +
4.50 +\subsection{Technische Voraussetzungen hergestellt: am 02.08.2010}
4.51 +\begin{itemize}
4.52 +\item Isabelle installiert, Filestruktur bekannt: am 02.08.2010
4.53 +\item Scala in NetBeans eingebunden: am 22.07.2010
4.54 +\item Mercurial installiert und einrichten des Repositories: 19.07.2010
4.55 +\end{itemize}
4.56 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.57 +\hline
4.58 +Datum & T\"atigkeit & Einheiten \\ \hline
4.59 +19.07.2010 & Beginn der Installationsarbeiten: Repo klonen und testen & 6 \\ \hline
4.60 +20.07.2010 & Installationsarbeiten, Einarbeiten in Filestruktur & 7 \\ \hline
4.61 +21.07.2010 & Einarbeiten in Filestruktur & 6 \\ \hline
4.62 +22.07.2010 & Vorbereitungen: NetBeans, JDK und Scala installieren. Scala in NetBeans integrieren & 8 \\ \hline
4.63 +23.07.2010 & Isabelle-jEdit-Plugin mittels NetBeans ausführen: testen & 5 \\ \hline
4.64 +27.07.2010 & Isabelle-jEdit-Plugin: Änderungen an der Projektstruktur & 7 \\ \hline
4.65 +28.07.2010 & Experimente mit Isabelle-jEdit-Plugin & 6 \\ \hline
4.66 +29.07.2010 & Identifikations der Parse-Einstiegsstelle & 5 \\ \hline
4.67 +30.07.2010 & Experimente mit Isabelle-jEdit-Plugin, Besprechung über Erfahrungen mit Filestruktur & 4 \\ \hline
4.68 +02.08.2010 & Installationen und einrichten des Repos auf meinen Laptop & 6 \\ \hline \hline
4.69 + & Anzahl der Einheiten & 60 \\
4.70 +\hline
4.71 +\end{tabular}
4.72 +
4.73 \subsection{NetBeans-Projekt aufgesetzt }% am ..(*)...}
4.74 +\begin{itemize}
4.75 +\item Grundlegende Projektstruktur f\"ur ISAC hergestellt: am 02.08.2010
4.76 +\item jEdit-Plugin: XML-Files für ISAC vorbereitet: am 22.07.2010
4.77 +\item jEdit-Plugin: Source files geschrieben: 19.07.2010
4.78 +\end{itemize}
4.79 +\begin{tabular}{|p{2cm}|p{8cm}|p{2cm}|}
4.80 +\hline
4.81 +Datum & T\"atigkeit & Einheiten \\ \hline
4.82 +10.08.2010 & Projektstruktur anlegen, build.xml anpassen & 7 \\ \hline
4.83 +11.08.2010 & jEdit-Plugin-Struktur studieren: Howto durcharbeiten & 5 \\ \hline
4.84 +21.08.2010 & bestehende jEdit-Plugins (Java) durcharbeiten & 3 \\ \hline
4.85 +22.08.2010 & Kopieren des Isabelle-jEdit-Plugins, Umarbeiten für ISAC & 3 \\ \hline
4.86 +24.08.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 6 \\ \hline
4.87 +26.08.2010 & Problem mit Isabelle-Umgebungsvariable: Suche nach Lösungen & 3 \\ \hline
4.88 +28.08.2010 & Recherchen zum Umgebungsvariable-Problem, Arbeiten mit den Isabelle-Shell-Skripts & 2 \\ \hline
4.89 +29.08.2010 & Experimente mit den Path-Varialbe der jvm & 3 \\ \hline
4.90 +30.08.2010 & Isabelle-jEdit-Plugin endlich vollständig lauffähig gebracht & 4 \\ \hline
4.91 +01.09.2010 & Arbeiten an der jEdit-ISAC-Projektstruktur & 3 \\ \hline
4.92 +04.09.2010 & Umarbeiten des Isabelle-Plugins für ISAC & 5 \\ \hline
4.93 +20.09.2010 & Einrichten des Laptops für Isabelle-Isac & 4 \\ \hline
4.94 +22.09.2010 & Meeting: Fortschrittsbericht, kurze Einführung für Mitstreiter & 3 \\ \hline
4.95 +
4.96 +29.09.2010 & Neue Vorgehensweise: QuickNotepad-Plugin(QN) wird in Scala übersetzt und für ISAC entsprechend angepasst: Arbeit an den XML-Files & 4 \\ \hline
4.97 +30.09.2010 & QN: Start mit übersetzten der Sourcefiles & 5 \\ \hline
4.98 +02.10.2010 & QN: Übersetzten der Sourcefiles & 6 \\ \hline
4.99 +04.10.2010 & QN: Übersetzten der Sourcefiles: Problem bei Interface & 3 \\ \hline
4.100 +05.10.2010 & QN: QN vollständig in Scala übersetzt, testen & 2 \\ \hline \hline
4.101 + & Anzahl der Einheiten & 71 \\
4.102 +\hline
4.103 +\end{tabular}
4.104 +
4.105 \subsection{Experimentelle Parser implementiert}% am ..(*)...}
4.106 \subsection{Pr\"asentation der Arbeit im IST-Seminar }% am ..(*)...}
4.107 %\newpage
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 12:45:58 2011 +0100
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 15:12:55 2011 +0100
5.3 @@ -32,11 +32,10 @@
5.4
5.5 ML {*
5.6 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
5.7 -val t = parseNEW ctxt "x + y = (y::int)";
5.8 +val t = parseNEW ctxt "x + 1 = (2::int)";
5.9 *}
5.10
5.11 ML {*
5.12 -tracing "\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>";
5.13 rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
5.14
5.15
6.1 --- a/src/Tools/isac/Test_Isac.thy Thu Mar 10 12:45:58 2011 +0100
6.2 +++ b/src/Tools/isac/Test_Isac.thy Thu Mar 10 15:12:55 2011 +0100
6.3 @@ -86,7 +86,7 @@
6.4 *}
6.5
6.6 ML {*Trueprop*}
6.7 -
6.8 +
6.9 ML {*
6.10
6.11 Config.put show_types true (thy2ctxt (@{theory "Isac"}))