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/Misc/ROOT.ML
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 13305 f88d0c363582
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9834
109b11c4e77e *** empty log message ***
nipkow
parents: 9722
diff changeset 
     1
 
use "../settings.ML";
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
     2
 
use_thy "Tree";
9493
494f8cd34df7 *** empty log message ***
nipkow
parents: 8745
diff changeset 
     3
 
use_thy "Tree2";
13305
f88d0c363582 *** empty log message ***
nipkow
parents: 12582
diff changeset 
     4
 
use_thy "Plus";
9721
7e51c9f3d5a0 *** empty log message ***
nipkow
parents: 9644
diff changeset 
     5
 
use_thy "case_exprs";
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
     6
 
use_thy "fakenat";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
     7
 
use_thy "natsum";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
     8
 
use_thy "pairs";
10543
8e4307d1207a *** empty log message ***
nipkow
parents: 10538
diff changeset 
     9
 
use_thy "Option2";
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
    10
 
use_thy "types";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
    11
 
use_thy "prime_def";
9844
8016321c7de1 *** empty log message ***
nipkow
parents: 9834
diff changeset 
    12
 
use_thy "simp";
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset 
    13
 
use_thy "Itrev";
9644
6b0b6b471855 *** empty log message ***
nipkow
parents: 9493
diff changeset 
    14
 
use_thy "AdvancedInd";
10978
5eebea8f359f *** empty log message ***
nipkow
parents: 10543
diff changeset 
    15
 
use_thy "appendix";
isabelle