src/HOL/Basic_BNFs.thy
changeset 55062 6d3fad6f01c9
parent 55058 4e700eb471d4
child 55075 b3d0a02a756d
     1.1 --- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4     (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
     1.5    Lifting_Sum
     1.6    Lifting_Product
     1.7 -  Main
     1.8  begin
     1.9  
    1.10  bnf ID: 'a