Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/mesontest2.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10440 2074e62da354
child 11586 d8a7f6318457
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10440
2074e62da354 proper theory context for mesontest2;
wenzelm
parents:
diff changeset 
     1
 












2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     2


(*Theory Product_Type instead of HOL regards arguments as tuples.













2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     3


  But theory Main would allow clashes with many other constants.*)













2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     4














2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     5


theory mesontest2 = Product_Type:













2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     6














2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     7


hide const inverse divide













2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     8














2074e62da354
proper theory context for mesontest2;



wenzelm


parents: 

diff
changeset




     9


end















isabelle