Check-in [71edd53195]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed some typos.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:71edd531956ef15e8715bce3fd5d3091782b3fe3
User & Date: andy 2015-04-28 21:18:16
Context
2015-04-30
07:06
Updated flyer with presentation location. check-in: 855f5cd0f0 user: andy tags: trunk
2015-04-28
21:18
Fixed some typos. check-in: 71edd53195 user: andy tags: trunk
21:13
Added presentation flyer files. check-in: c387492ea6 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to flyer/arend-flyer.pdf.

cannot compute difference between binary files

Changes to flyer/arend-flyer.sla.

23
24
25
26
27
28
29
30







31
32
33
34
35
36
37
..
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
..
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
        <STYLE NAME="Bullets" PARENT="Default Paragraph Style" INDENT="26" FIRST="-26" CPARENT="Default Character Style" FCOLOR="Red">
            <Tabs Type="0" Pos="26" Fill=""/>
            <Tabs Type="0" Pos="49" Fill=""/>
        </STYLE>
        <CHARSTYLE CNAME="Default Character Style" DefaultStyle="1" FONT="Arial Regular" FONTSIZE="12" FEATURES="inherit" FCOLOR="Black" FSHADE="100" SCOLOR="Black" SSHADE="100" TXTSHX="5" TXTSHY="-5" TXTOUT="1" TXTULP="-0.1" TXTULW="-0.1" TXTSTP="-0.1" TXTSTW="-0.1" SCALEH="100" SCALEV="100" BASEO="0" KERN="0" LANGUAGE="English"/>
        <LAYERS NUMMER="0" LEVEL="0" NAME="Background" SICHTBAR="1" DRUCKEN="1" EDIT="1" FLOW="1" TRANS="1" BLEND="0" OUTL="0" LAYERC="#000000"/>
        <Printer firstUse="1" toFile="0" useAltPrintCommand="0" outputSeparations="0" useSpotColors="0" useColor="0" mirrorH="0" mirrorV="0" useICC="0" doGCR="0" doClip="0" setDevParam="0" useDocBleeds="0" cropMarks="0" bleedMarks="240" registrationMarks="63" colorMarks="0" includePDFMarks="0" PSLevel="0" PDLanguage="0" markOffset="1" BleedTop="0" BleedLeft="0" BleedRight="0" BleedBottom="0" printer="" filename="" separationName="" printerCommand=""/>
        <PDF firstUse="1" Thumbnails="0" Articles="0" Bookmarks="0" Compress="1" CMethod="0" Quality="0" MirrorH="0" MirrorV="0" Clip="0" RotateDeg="0" PresentMode="0" RecalcPic="0" Grayscale="0" RGBMode="1" UseProfiles="0" UseProfiles2="0" Binding="0" PicRes="300" Resolution="300" Version="14" Intent="1" Intent2="0" SolidP="CineonLog M " ImageP="CineonLog M " PrintP="Fogra27L CMYK Coated Press" InfoString="" BTop="0" BLeft="0" BRight="0" BBottom="0" useDocBleeds="1" cropMarks="0" bleedMarks="0" registrationMarks="0" colorMarks="0" docInfoMarks="0" markOffset="0" ImagePr="0" PassOwner="" PassUser="" Permissions="-4" Encrypt="0" UseLayers="0" UseLpi="0" UseSpotColors="1" doMultiFile="0" displayBookmarks="0" displayFullscreen="0" displayLayers="0" displayThumbs="0" hideMenuBar="0" hideToolBar="0" fitWindow="0" PageLayout="0" openAction="">







            <LPI Color="Black" Frequency="133" Angle="45" SpotFunction="3"/>
            <LPI Color="Cyan" Frequency="133" Angle="105" SpotFunction="3"/>
            <LPI Color="Magenta" Frequency="133" Angle="75" SpotFunction="3"/>
            <LPI Color="Yellow" Frequency="133" Angle="90" SpotFunction="3"/>
        </PDF>
        <DocItemAttributes/>
        <TablesOfContents/>
................................................................................
            <Section Number="0" Name="0" From="0" To="0" Type="Type_1_2_3" Start="1" Reversed="0" Active="1"/>
        </Sections>
        <MASTERPAGE PAGEXPOS="100" PAGEYPOS="20" PAGEWIDTH="612" PAGEHEIGHT="792" BORDERLEFT="40" BORDERRIGHT="40" BORDERTOP="40" BORDERBOTTOM="40" NUM="0" NAM="Normal" MNAM="" Size="Letter" Orientation="0" LEFT="0" PRESET="0" VerticalGuides="" HorizontalGuides="" AGhorizontalAutoGap="0" AGverticalAutoGap="0" AGhorizontalAutoCount="0" AGverticalAutoCount="0" AGhorizontalAutoRefer="0" AGverticalAutoRefer="0" AGSelection="0 0 0 0"/>
        <PAGE PAGEXPOS="100" PAGEYPOS="20" PAGEWIDTH="612" PAGEHEIGHT="792" BORDERLEFT="40" BORDERRIGHT="40" BORDERTOP="40" BORDERBOTTOM="40" NUM="0" NAM="" MNAM="Normal" Size="Letter" Orientation="0" LEFT="0" PRESET="0" VerticalGuides="" HorizontalGuides="" AGhorizontalAutoGap="0" AGverticalAutoGap="0" AGhorizontalAutoCount="0" AGverticalAutoCount="0" AGhorizontalAutoRefer="0" AGverticalAutoRefer="0" AGSelection="0 0 0 0"/>
        <PAGEOBJECT OwnPage="0" PTYPE="4" XPOS="318.75" YPOS="62" WIDTH="349.75" HEIGHT="319.75" RADRECT="0" FRTYPE="0" CLIPEDIT="0" PWIDTH="1" PCOLOR="None" PCOLOR2="None" COLUMNS="1" COLGAP="0" NAMEDLST="" SHADE="100" SHADE2="100" GRTYP="0" ROT="0" PLINEART="1" PLINEEND="0" PLINEJOIN="0" LOCALSCX="1" LOCALSCY="1" LOCALX="0" LOCALY="0" PICART="1" PLTSHOW="0" BASEOF="0" textPathType="0" textPathFlipped="0" FLIPPEDH="0" FLIPPEDV="0" SCALETYPE="1" RATIO="1" PRINTABLE="1" ANNOTATION="0" ANNAME="" TEXTFLOWMODE="0" TEXTFLOW="0" TEXTFLOW2="0" TEXTFLOW3="0" AUTOTEXT="0" EXTRA="0" TEXTRA="0" BEXTRA="0" REXTRA="0" FLOP="0" PFILE="" PFILE2="" PFILE3="" PRFILE="" EPROF="" IRENDER="1" EMBEDDED="1" LOCK="0" LOCKR="0" REVERS="0" TransValue="0" TransValueS="0" TransBlend="0" TransBlendS="0" isTableItem="0" TopLine="0" LeftLine="0" RightLine="0" BottomLine="0" isGroupControl="0" NUMDASH="0" DASHS="" DASHOFF="0" NUMPO="16" POCOOR="0 0 0 0 349.75 0 349.75 0 349.75 0 349.75 0 349.75 319.75 349.75 319.75 349.75 319.75 349.75 319.75 0 319.75 0 319.75 0 319.75 0 319.75 0 0 0 0 " NUMCO="16" COCOOR="0 0 0 0 349.75 0 349.75 0 349.75 0 349.75 0 349.75 319.75 349.75 319.75 349.75 319.75 349.75 319.75 0 319.75 0 319.75 0 319.75 0 319.75 0 0 0 0 " NUMGROUP="0" GROUPS="" startArrowIndex="0" endArrowIndex="0" OnMasterPage="" ImageClip="" ImageRes="1" Pagenumber="0" isInline="0" fillRule="1" doOverprint="0" gXpos="0" gYpos="0" gWidth="0" gHeight="0" LAYER="0" BOOKMARK="0" NEXTITEM="-1" BACKITEM="-1">
            <ITEXT FONT="Cabin Italic" FONTSIZE="15" CH="Proofs. "/>
            <para ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="The very word is often enough to strike fear into the fragile soul of a computer science undergraduate. Even worse is the task itself: perhaps you remember working late into the night, toiling over some logical monstrosity. You turn it in, and a week (or two, or three) later, it is returned to you, slashed and scrawled with some TA's comments, in blood-red ink — or is it actual blood? — the margins filled with such wounding and hurtful comments as "/>
            <para ALIGN="3"/>
            <para ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="•"/>
            <tab FONT="Cabin Regular" FONTSIZE="12"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="&quot;Wrong&quot;"/>
            <para PARENT="Bullets" ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="•"/>
................................................................................
            <para ALIGN="3"/>
            <PageItemAttributes/>
        </PAGEOBJECT>
        <PAGEOBJECT OwnPage="0" PTYPE="4" XPOS="175" YPOS="395.5" WIDTH="461" HEIGHT="376" RADRECT="0" FRTYPE="0" CLIPEDIT="0" PWIDTH="1" PCOLOR="None" PCOLOR2="None" COLUMNS="1" COLGAP="0" NAMEDLST="" SHADE="100" SHADE2="100" GRTYP="0" ROT="0" PLINEART="1" PLINEEND="0" PLINEJOIN="0" LOCALSCX="1" LOCALSCY="1" LOCALX="0" LOCALY="0" PICART="1" PLTSHOW="0" BASEOF="0" textPathType="0" textPathFlipped="0" FLIPPEDH="0" FLIPPEDV="0" SCALETYPE="1" RATIO="1" PRINTABLE="1" ANNOTATION="0" ANNAME="" TEXTFLOWMODE="0" TEXTFLOW="0" TEXTFLOW2="0" TEXTFLOW3="0" AUTOTEXT="0" EXTRA="0" TEXTRA="0" BEXTRA="0" REXTRA="0" FLOP="0" PFILE="" PFILE2="" PFILE3="" PRFILE="" EPROF="" IRENDER="1" EMBEDDED="1" LOCK="0" LOCKR="0" REVERS="0" TransValue="0" TransValueS="0" TransBlend="0" TransBlendS="0" isTableItem="0" TopLine="0" LeftLine="0" RightLine="0" BottomLine="0" isGroupControl="0" NUMDASH="0" DASHS="" DASHOFF="0" NUMPO="16" POCOOR="0 0 0 0 461 0 461 0 461 0 461 0 461 376 461 376 461 376 461 376 0 376 0 376 0 376 0 376 0 0 0 0 " NUMCO="16" COCOOR="0 0 0 0 461 0 461 0 461 0 461 0 461 376 461 376 461 376 461 376 0 376 0 376 0 376 0 376 0 0 0 0 " NUMGROUP="0" GROUPS="" startArrowIndex="0" endArrowIndex="0" OnMasterPage="" ImageClip="" ImageRes="1" Pagenumber="0" isInline="0" fillRule="1" doOverprint="0" gXpos="0" gYpos="0" gWidth="0" gHeight="0" LAYER="0" BOOKMARK="0" NEXTITEM="-1" BACKITEM="-1">
            <ITEXT FONT="Junicode Regular" FONTSIZE="15" CH="Arend — Proof-assistant Assisted Pedagogy"/>
            <para ALIGN="1"/>
            <para/>
            <ITEXT FONT="Junicode Regular" CH="Arend is a proof assistant designed for use in undergraduate computer science curriculum. While proof assistants, and even their use in graduate-level work, are not novel, their use at the undergraduate level has been surprisingly unexplored. Arend offers"/>
            <para ALIGN="3"/>
            <para PARENT="Bullets" ALIGN="3"/>
            <ITEXT FONT="Junicode Regular" FCOLOR="Black" FSHADE="100" CH="•"/>
            <tab FONT="Junicode Regular" FCOLOR="Black" FSHADE="100"/>
            <ITEXT FONT="Junicode Regular" FCOLOR="Black" FSHADE="100" CH="An intuitive graphical interface, where both specifications and the proofs about them are displayed as inference rules and trees of rule-applications called derivations. Proofs are constructed non-linearly, in any order the student prefers, and the completeness, or lack thereof, of a proof is always obvious."/>
            <para PARENT="Bullets" ALIGN="3"/>
            <para ALIGN="3"/>







|
>
>
>
>
>
>
>







 







|







 







|







23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
..
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
..
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
        <STYLE NAME="Bullets" PARENT="Default Paragraph Style" INDENT="26" FIRST="-26" CPARENT="Default Character Style" FCOLOR="Red">
            <Tabs Type="0" Pos="26" Fill=""/>
            <Tabs Type="0" Pos="49" Fill=""/>
        </STYLE>
        <CHARSTYLE CNAME="Default Character Style" DefaultStyle="1" FONT="Arial Regular" FONTSIZE="12" FEATURES="inherit" FCOLOR="Black" FSHADE="100" SCOLOR="Black" SSHADE="100" TXTSHX="5" TXTSHY="-5" TXTOUT="1" TXTULP="-0.1" TXTULW="-0.1" TXTSTP="-0.1" TXTSTW="-0.1" SCALEH="100" SCALEV="100" BASEO="0" KERN="0" LANGUAGE="English"/>
        <LAYERS NUMMER="0" LEVEL="0" NAME="Background" SICHTBAR="1" DRUCKEN="1" EDIT="1" FLOW="1" TRANS="1" BLEND="0" OUTL="0" LAYERC="#000000"/>
        <Printer firstUse="1" toFile="0" useAltPrintCommand="0" outputSeparations="0" useSpotColors="0" useColor="0" mirrorH="0" mirrorV="0" useICC="0" doGCR="0" doClip="0" setDevParam="0" useDocBleeds="0" cropMarks="0" bleedMarks="240" registrationMarks="63" colorMarks="0" includePDFMarks="0" PSLevel="0" PDLanguage="0" markOffset="1" BleedTop="0" BleedLeft="0" BleedRight="0" BleedBottom="0" printer="" filename="" separationName="" printerCommand=""/>
        <PDF firstUse="0" Thumbnails="0" Articles="0" Bookmarks="0" Compress="1" CMethod="0" Quality="0" MirrorH="0" MirrorV="0" Clip="0" RotateDeg="0" PresentMode="0" RecalcPic="0" Grayscale="0" RGBMode="1" UseProfiles="0" UseProfiles2="0" Binding="0" PicRes="300" Resolution="300" Version="14" Intent="1" Intent2="0" SolidP="CineonLog M " ImageP="CineonLog M " PrintP="Fogra27L CMYK Coated Press" InfoString="" BTop="0" BLeft="0" BRight="0" BBottom="0" useDocBleeds="1" cropMarks="0" bleedMarks="0" registrationMarks="0" colorMarks="0" docInfoMarks="0" markOffset="0" ImagePr="0" PassOwner="" PassUser="" Permissions="-4" Encrypt="0" UseLayers="0" UseLpi="0" UseSpotColors="1" doMultiFile="0" displayBookmarks="0" displayFullscreen="0" displayLayers="0" displayThumbs="0" hideMenuBar="0" hideToolBar="0" fitWindow="0" PageLayout="0" openAction="">
            <Fonts Name="Arial Regular"/>
            <Fonts Name="Junicode Bold"/>
            <Subset Name="Cabin Italic"/>
            <Subset Name="Cabin Regular"/>
            <Subset Name="Junicode Regular"/>
            <Effekte pageEffectDuration="1" pageViewDuration="1" effectType="0" Dm="0" M="0" Di="0"/>
            <LPI Color="" Frequency="133" Angle="45" SpotFunction="3"/>
            <LPI Color="Black" Frequency="133" Angle="45" SpotFunction="3"/>
            <LPI Color="Cyan" Frequency="133" Angle="105" SpotFunction="3"/>
            <LPI Color="Magenta" Frequency="133" Angle="75" SpotFunction="3"/>
            <LPI Color="Yellow" Frequency="133" Angle="90" SpotFunction="3"/>
        </PDF>
        <DocItemAttributes/>
        <TablesOfContents/>
................................................................................
            <Section Number="0" Name="0" From="0" To="0" Type="Type_1_2_3" Start="1" Reversed="0" Active="1"/>
        </Sections>
        <MASTERPAGE PAGEXPOS="100" PAGEYPOS="20" PAGEWIDTH="612" PAGEHEIGHT="792" BORDERLEFT="40" BORDERRIGHT="40" BORDERTOP="40" BORDERBOTTOM="40" NUM="0" NAM="Normal" MNAM="" Size="Letter" Orientation="0" LEFT="0" PRESET="0" VerticalGuides="" HorizontalGuides="" AGhorizontalAutoGap="0" AGverticalAutoGap="0" AGhorizontalAutoCount="0" AGverticalAutoCount="0" AGhorizontalAutoRefer="0" AGverticalAutoRefer="0" AGSelection="0 0 0 0"/>
        <PAGE PAGEXPOS="100" PAGEYPOS="20" PAGEWIDTH="612" PAGEHEIGHT="792" BORDERLEFT="40" BORDERRIGHT="40" BORDERTOP="40" BORDERBOTTOM="40" NUM="0" NAM="" MNAM="Normal" Size="Letter" Orientation="0" LEFT="0" PRESET="0" VerticalGuides="" HorizontalGuides="" AGhorizontalAutoGap="0" AGverticalAutoGap="0" AGhorizontalAutoCount="0" AGverticalAutoCount="0" AGhorizontalAutoRefer="0" AGverticalAutoRefer="0" AGSelection="0 0 0 0"/>
        <PAGEOBJECT OwnPage="0" PTYPE="4" XPOS="318.75" YPOS="62" WIDTH="349.75" HEIGHT="319.75" RADRECT="0" FRTYPE="0" CLIPEDIT="0" PWIDTH="1" PCOLOR="None" PCOLOR2="None" COLUMNS="1" COLGAP="0" NAMEDLST="" SHADE="100" SHADE2="100" GRTYP="0" ROT="0" PLINEART="1" PLINEEND="0" PLINEJOIN="0" LOCALSCX="1" LOCALSCY="1" LOCALX="0" LOCALY="0" PICART="1" PLTSHOW="0" BASEOF="0" textPathType="0" textPathFlipped="0" FLIPPEDH="0" FLIPPEDV="0" SCALETYPE="1" RATIO="1" PRINTABLE="1" ANNOTATION="0" ANNAME="" TEXTFLOWMODE="0" TEXTFLOW="0" TEXTFLOW2="0" TEXTFLOW3="0" AUTOTEXT="0" EXTRA="0" TEXTRA="0" BEXTRA="0" REXTRA="0" FLOP="0" PFILE="" PFILE2="" PFILE3="" PRFILE="" EPROF="" IRENDER="1" EMBEDDED="1" LOCK="0" LOCKR="0" REVERS="0" TransValue="0" TransValueS="0" TransBlend="0" TransBlendS="0" isTableItem="0" TopLine="0" LeftLine="0" RightLine="0" BottomLine="0" isGroupControl="0" NUMDASH="0" DASHS="" DASHOFF="0" NUMPO="16" POCOOR="0 0 0 0 349.75 0 349.75 0 349.75 0 349.75 0 349.75 319.75 349.75 319.75 349.75 319.75 349.75 319.75 0 319.75 0 319.75 0 319.75 0 319.75 0 0 0 0 " NUMCO="16" COCOOR="0 0 0 0 349.75 0 349.75 0 349.75 0 349.75 0 349.75 319.75 349.75 319.75 349.75 319.75 349.75 319.75 0 319.75 0 319.75 0 319.75 0 319.75 0 0 0 0 " NUMGROUP="0" GROUPS="" startArrowIndex="0" endArrowIndex="0" OnMasterPage="" ImageClip="" ImageRes="1" Pagenumber="0" isInline="0" fillRule="1" doOverprint="0" gXpos="0" gYpos="0" gWidth="0" gHeight="0" LAYER="0" BOOKMARK="0" NEXTITEM="-1" BACKITEM="-1">
            <ITEXT FONT="Cabin Italic" FONTSIZE="15" CH="Proofs. "/>
            <para ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="The very word is often enough to strike fear into the fragile soul of a computer science undergraduate. Even worse is the task itself: perhaps you remember working late into the night, toiling over some logical monstrosity. You turn it in, and a week (or two, or three) later, it is returned to you, slashed and scrawled with some TA's criticism, in blood-red ink — or is it actual blood? — the margins filled with such wounding and hurtful comments as "/>
            <para ALIGN="3"/>
            <para ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="•"/>
            <tab FONT="Cabin Regular" FONTSIZE="12"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="&quot;Wrong&quot;"/>
            <para PARENT="Bullets" ALIGN="3"/>
            <ITEXT FONT="Cabin Regular" FONTSIZE="12" CH="•"/>
................................................................................
            <para ALIGN="3"/>
            <PageItemAttributes/>
        </PAGEOBJECT>
        <PAGEOBJECT OwnPage="0" PTYPE="4" XPOS="175" YPOS="395.5" WIDTH="461" HEIGHT="376" RADRECT="0" FRTYPE="0" CLIPEDIT="0" PWIDTH="1" PCOLOR="None" PCOLOR2="None" COLUMNS="1" COLGAP="0" NAMEDLST="" SHADE="100" SHADE2="100" GRTYP="0" ROT="0" PLINEART="1" PLINEEND="0" PLINEJOIN="0" LOCALSCX="1" LOCALSCY="1" LOCALX="0" LOCALY="0" PICART="1" PLTSHOW="0" BASEOF="0" textPathType="0" textPathFlipped="0" FLIPPEDH="0" FLIPPEDV="0" SCALETYPE="1" RATIO="1" PRINTABLE="1" ANNOTATION="0" ANNAME="" TEXTFLOWMODE="0" TEXTFLOW="0" TEXTFLOW2="0" TEXTFLOW3="0" AUTOTEXT="0" EXTRA="0" TEXTRA="0" BEXTRA="0" REXTRA="0" FLOP="0" PFILE="" PFILE2="" PFILE3="" PRFILE="" EPROF="" IRENDER="1" EMBEDDED="1" LOCK="0" LOCKR="0" REVERS="0" TransValue="0" TransValueS="0" TransBlend="0" TransBlendS="0" isTableItem="0" TopLine="0" LeftLine="0" RightLine="0" BottomLine="0" isGroupControl="0" NUMDASH="0" DASHS="" DASHOFF="0" NUMPO="16" POCOOR="0 0 0 0 461 0 461 0 461 0 461 0 461 376 461 376 461 376 461 376 0 376 0 376 0 376 0 376 0 0 0 0 " NUMCO="16" COCOOR="0 0 0 0 461 0 461 0 461 0 461 0 461 376 461 376 461 376 461 376 0 376 0 376 0 376 0 376 0 0 0 0 " NUMGROUP="0" GROUPS="" startArrowIndex="0" endArrowIndex="0" OnMasterPage="" ImageClip="" ImageRes="1" Pagenumber="0" isInline="0" fillRule="1" doOverprint="0" gXpos="0" gYpos="0" gWidth="0" gHeight="0" LAYER="0" BOOKMARK="0" NEXTITEM="-1" BACKITEM="-1">
            <ITEXT FONT="Junicode Regular" FONTSIZE="15" CH="Arend — Proof-assistant Assisted Pedagogy"/>
            <para ALIGN="1"/>
            <para/>
            <ITEXT FONT="Junicode Regular" CH="Arend is a proof assistant designed for use in the undergraduate computer science curriculum. While proof assistants, and even their use in graduate-level work, are not novel, their use at the undergraduate level has been surprisingly unexplored. Arend offers"/>
            <para ALIGN="3"/>
            <para PARENT="Bullets" ALIGN="3"/>
            <ITEXT FONT="Junicode Regular" FCOLOR="Black" FSHADE="100" CH="•"/>
            <tab FONT="Junicode Regular" FCOLOR="Black" FSHADE="100"/>
            <ITEXT FONT="Junicode Regular" FCOLOR="Black" FSHADE="100" CH="An intuitive graphical interface, where both specifications and the proofs about them are displayed as inference rules and trees of rule-applications called derivations. Proofs are constructed non-linearly, in any order the student prefers, and the completeness, or lack thereof, of a proof is always obvious."/>
            <para PARENT="Bullets" ALIGN="3"/>
            <para ALIGN="3"/>