--- a/src/HOL/Tools/record_package.ML Wed Jul 24 17:59:12 2002 +0200
+++ b/src/HOL/Tools/record_package.ML Wed Jul 24 22:13:02 2002 +0200
@@ -45,7 +45,7 @@
val product_typeN = "Record.product_type";
-val product_typeI = thm "product_typeI";
+val product_type_intro = thm "product_type.intro";
val product_type_inject = thm "product_type.inject";
val product_type_conv1 = thm "product_type.conv1";
val product_type_conv2 = thm "product_type.conv2";
@@ -621,7 +621,7 @@
|>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1
|>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2;
- val prod_types = map (fn (((a, b), c), d) => product_typeI OF [a, b, c, d])
+ val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d])
(typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2);
--- a/src/HOL/ex/Locales.thy Wed Jul 24 17:59:12 2002 +0200
+++ b/src/HOL/ex/Locales.thy Wed Jul 24 22:13:02 2002 +0200
@@ -233,7 +233,11 @@
exhibited directly as context parameters; logically this corresponds
to a curried predicate definition:
- @{thm [display] group_context_axioms_def [no_vars]}
+ @{thm [display] group_context_def [no_vars]}
+
+ The corresponding introduction rule is as follows:
+
+ @{thm [display] group_context.intro [no_vars]}
Occasionally, this ``externalized'' version of the informal idea of
classes of tuple structures may cause some inconveniences,