# HG changeset patch
# User wenzelm
# Date 1113410725 -7200
# Node ID b5edb9dcec9ad1b09812cc846db4fc75099314bc
# Parent  93163972dbdcfb0fa1e650885c9e1e898269d6d8
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;

diff -r 93163972dbdc -r b5edb9dcec9a src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -916,3 +916,4 @@
 end;
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -301,3 +301,4 @@
 
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -382,3 +382,4 @@
 
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/Pure/Isar/constdefs.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -83,3 +83,4 @@
   ProofContext.cert_typ ProofContext.cert_term (K I);
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -450,3 +450,4 @@
 end;
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -445,3 +445,4 @@
 end;
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -95,3 +95,4 @@
 end;
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -232,3 +232,4 @@
 
 val exhaust_tac = DatatypeTactics.exhaust_tac;
 val induct_tac  = DatatypeTactics.induct_tac;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -622,3 +622,4 @@
 end;
 
 end;
+
diff -r 93163972dbdc -r b5edb9dcec9a src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Apr 13 18:45:09 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Wed Apr 13 18:45:25 2005 +0200
@@ -213,3 +213,5 @@
 end;
 
 end;
+
+