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.
ProtoPure.flexpair_def;
authorwenzelm
Fri, 24 Oct 1997 17:25:33 +0200
changeset 4000 0614fdf0db20
parent 3999 86c5bda38e9f
child 4001 b6a3c2665c45
ProtoPure.flexpair_def;
src/HOL/NatDef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/NatDef.ML	Fri Oct 24 17:19:14 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Oct 24 17:25:33 1997 +0200
@@ -77,7 +77,7 @@
   exhaustion = natE,
   exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
                                        (rotate_tac ~1),
-  nchotomy = flexpair_def, case_cong = flexpair_def})];
+  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})];
 
 
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
isabelle