Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Primrec: New example ported from ZF
authorpaulson
Mon, 26 May 1997 12:34:05 +0200
changeset 3337 c056d328aa0e
parent 3336 29ddef80bd49
child 3338 b99d750f6a37
Primrec: New example ported from ZF
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Mon May 26 12:33:38 1997 +0200
+++ b/src/HOL/IsaMakefile	Mon May 26 12:34:05 1997 +0200
@@ -200,7 +200,7 @@
 
 ## Miscellaneous examples
 
-EX_NAMES = Fib Primes NatSum String BT InSort Qsort Puzzle MT
+EX_NAMES = Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- a/src/HOL/ex/ROOT.ML	Mon May 26 12:33:38 1997 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon May 26 12:34:05 1997 +0200
@@ -14,6 +14,7 @@
 (**Some examples of recursive function definitions: the TFL package**)
 time_use_thy "Fib";
 time_use_thy "Primes";
+time_use_thy "Primrec";
 
 time_use_thy "NatSum";
 time_use     "cla.ML";
isabelle