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/Inductive.thy
author paulson
Tue, 21 Sep 1999 11:11:09 +0200
changeset 7547 a72a551b6d79
parent 7357 d0e16da40ea2
child 7700 38b6d2643630
permissions -rw-r--r--
new proof of drop_prog_correct for new definition of project_act
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset 
     1
 







7357






d0e16da40ea2
proper bootstrap of HOL theory and packages;



wenzelm


parents: 
6437

diff
changeset




     2


theory Inductive = Gfp + Prod + Sum













d0e16da40ea2
proper bootstrap of HOL theory and packages;



wenzelm


parents: 
6437

diff
changeset




     3


files "Tools/inductive_package.ML":








6437






9bdfe07ba8e9
'HOL/inductive' theory data;



wenzelm


parents: 
5105

diff
changeset




     4














9bdfe07ba8e9
'HOL/inductive' theory data;



wenzelm


parents: 
5105

diff
changeset




     5


setup InductivePackage.setup













9bdfe07ba8e9
'HOL/inductive' theory data;



wenzelm


parents: 
5105

diff
changeset




     6














9bdfe07ba8e9
'HOL/inductive' theory data;



wenzelm


parents: 
5105

diff
changeset




     7


end















isabelle