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.
doc-src/TutorialI/Inductive/ROOT.ML
author blanchet
Tue, 17 Feb 2009 14:01:54 +0100
changeset 29956 62f931b257b7
parent 10762 cd1a2bee5549
permissions -rw-r--r--
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents:
diff changeset 
     1
 
use "../settings.ML";
10341
6eb91805a012 added the $Id:$ line
paulson
parents: 10225
diff changeset 
     2
 
use_thy "Even";
10762
cd1a2bee5549 *** empty log message ***
nipkow
parents: 10368
diff changeset 
     3
 
use_thy "Mutual";
10225
b9fd52525b69 *** empty log message ***
nipkow
parents: 10217
diff changeset 
     4
 
use_thy "Star";
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents:
diff changeset 
     5
 
use_thy "AB";
10368
f7e8abd8ea15 replaced Acc.thy by Advanced.thy
paulson
parents: 10341
diff changeset 
     6
 
use_thy "Advanced";
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents:
diff changeset 
     7
 














isabelle