src/HOL/Metis_Examples/Message.thy
changeset 42463 f270e3e18be5
parent 42103 6066a35f6678
child 43197 c71657bbdbc0
     1.1 --- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Message.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -14,8 +14,7 @@
     1.4  lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
     1.5  by (metis Un_commute Un_left_absorb)
     1.6  
     1.7 -types 
     1.8 -  key = nat
     1.9 +type_synonym key = nat
    1.10  
    1.11  consts
    1.12    all_symmetric :: bool        --{*true if all keys are symmetric*}