src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
changeset 55087 252c7fec4119
parent 55075 b3d0a02a756d
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 21:45:08 2014 +0100
     1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 22:24:48 2014 +0100
     1.3 @@ -681,8 +681,6 @@
     1.4  
     1.5  subsection{* Regular Trees *}
     1.6  
     1.7 -hide_const regular
     1.8 -
     1.9  definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
    1.10  definition "regular tr \<equiv> \<exists> f. reg f tr"
    1.11