Mercurial Mercurial > hg > isabelle-cookbook / 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.
CookBook/infix_conv.ML
author Christian Urban <urbanc@in.tum.de>
Wed, 04 Mar 2009 13:15:29 +0000
changeset 157 76cdc8f562fc
parent 142 c06885c36575
permissions -rw-r--r--
added more to the simplifier section
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
142
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     1
 
signature INFIX_CONV =
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     2
 
sig
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     3
 
  val then_conv : Thm.conv * Thm.conv -> Thm.conv
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     4
 
  val else_conv : Thm.conv * Thm.conv -> Thm.conv
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     5
 
end
c06885c36575 Polished conversion section.
boehmes
parents:
diff changeset 
     6
 












c06885c36575
Polished conversion section.



boehmes


parents: 

diff
changeset




     7


structure InfixConv : INFIX_CONV = Conv













c06885c36575
Polished conversion section.



boehmes


parents: 

diff
changeset




     8














c06885c36575
Polished conversion section.



boehmes


parents: 

diff
changeset




     9


open InfixConv















isabelle-cookbook