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.
* ZF: new-style theory commands 'inductive', 'inductive_cases', and
authorwenzelm
Tue, 13 Nov 2001 22:25:59 +0100
changeset 12177 b1c16d685a99
parent 12176 f9139e09a983
child 12178 06c3d9a884c5
* ZF: new-style theory commands 'inductive', 'inductive_cases', and methods 'ind_cases', 'induct_tac', 'case_tac';
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Tue Nov 13 22:24:28 2001 +0100
+++ b/NEWS	Tue Nov 13 22:25:59 2001 +0100
@@ -209,14 +209,17 @@
 
 *** ZF ***
 
+* ZF: new-style theory commands 'inductive', 'inductive_cases', and
+methods 'ind_cases', 'induct_tac', 'case_tac';
+
 * ZF: the integer library now covers quotients and remainders, with
 many laws relating division to addition, multiplication, etc.;
 
-* ZF/Induct: new directory for examples of inductive definitions, including theory
-Multiset for multiset orderings;
-
-* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless
-version of the formalism;
+* ZF/Induct: new directory for examples of inductive definitions,
+including theory Multiset for multiset orderings;
+
+* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
+typeless version of the formalism;
 
 
 *** General ***
isabelle