src/Doc/IsarImplementation/Base.thy
author blanchet
Fri, 28 Sep 2012 15:14:11 +0200
changeset 49642 9f884142334c
parent 48985 5386df44a037
child 56059 2390391584c2
permissions -rw-r--r--
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"

theory Base
imports Main
begin

ML_file "../antiquote_setup.ML"
setup {* Antiquote_Setup.setup *}

end