src/HOL/ex/mesontest2.thy
changeset 10440 2074e62da354
child 11586 d8a7f6318457
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/mesontest2.thy	Fri Nov 10 19:08:30 2000 +0100
@@ -0,0 +1,9 @@
+
+(*Theory Product_Type instead of HOL regards arguments as tuples.
+  But theory Main would allow clashes with many other constants.*)
+
+theory mesontest2 = Product_Type:
+
+hide const inverse divide
+
+end