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/ROOT.ML
author wenzelm
Mon, 12 Jul 1999 22:27:20 +0200
changeset 6981 eaade7e398a7
parent 6882 fe4e3d26fa8f
child 7384 33c976216121
permissions -rw-r--r--
export assumption_tac; local qeds: print rule; same_tac: actually insert rules, !! bind vars;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset 
     1
 
(*  Title:      HOL/Isar_examples/ROOT.ML
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset 
     2
 
    ID:         $Id$
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset 
     3
 
    Author:     Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset 
     4
 












2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




     5


Miscellaneous Isabelle/Isar examples for Higher-Order Logic.













2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




     6


*)













2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




     7














2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




     8


use_thy "BasicLogic";













2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




     9


use_thy "Peirce";













2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




    10


use_thy "Cantor";













2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.



wenzelm


parents: 

diff
changeset




    11


use_thy "ExprCompiler";








6765






6eba3d69037b
added Group.thy;



wenzelm


parents: 
6559

diff
changeset




    12


use_thy "Group";








6526






6b64d1454ee3
added Isar_examples/NatSum.thy;



wenzelm


parents: 
6444

diff
changeset




    13


use_thy "NatSum";








6882






fe4e3d26fa8f
added KnasterTarski.thy;



wenzelm


parents: 
6765

diff
changeset




    14


use_thy "KnasterTarski";















isabelle