Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Isar_Examples/README.html
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 36862 952b2b102a0a
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 7804
diff changeset 
     1
 
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 7804
diff changeset 
     2
 







7005






cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




     3


<html>













cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




     4














cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




     5


<head>








15582






7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     6


  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">








33026






8f35633c4922
modernized session Isar_Examples;



wenzelm


parents: 
15582

diff
changeset




     7


  <title>HOL/Isar_Examples</title>








7005






cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




     8


</head>













cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




     9














cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




    10


<body>








33026






8f35633c4922
modernized session Isar_Examples;



wenzelm


parents: 
15582

diff
changeset




    11


<h1>HOL/Isar_Examples</h1>








7005






cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




    12














cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




    13


Isar offers a new high-level proof (and theory) language interface to













cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




    14


Isabelle.  This directory contains some example Isar documents.  See








7804






80706fa84622
improved;



wenzelm


parents: 
7740

diff
changeset




    15


also the included document, or the <a













80706fa84622
improved;



wenzelm


parents: 
7740

diff
changeset




    16


href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more













80706fa84622
improved;



wenzelm


parents: 
7740

diff
changeset




    17


information.













80706fa84622
improved;



wenzelm


parents: 
7740

diff
changeset




    18


</body>








7005






cc778d613217
tuned comments;



wenzelm


parents: 

diff
changeset




    19


</html>















isabelle