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