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/Integ/NatSimprocs.thy
author wenzelm
Fri, 28 Sep 2001 19:17:01 +0200
changeset 11626 0dbfb578bf75
parent 10536 8f34ecae1446
child 14128 fd6d20c2371c
permissions -rw-r--r--
recdef (permissive);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10536
8f34ecae1446 invoking CancelNumeralFactorFun
paulson
parents: 9436
diff changeset 
     1
 
(*Loading further simprocs*)
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 8858
diff changeset 
     2
 
theory NatSimprocs = NatBin
10536
8f34ecae1446 invoking CancelNumeralFactorFun
paulson
parents: 9436
diff changeset 
     3
 
files "int_factor_simprocs.ML" "nat_simprocs.ML":
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 8858
diff changeset 
     4
 












62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;



wenzelm


parents: 
8858

diff
changeset




     5


setup nat_simprocs_setup













62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;



wenzelm


parents: 
8858

diff
changeset




     6









8858






b739f0ecc1fa
new dummy theory; prevents strange errors when loading NatSimprocs.ML



paulson


parents: 

diff
changeset




     7


end















isabelle