cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
(* Title: HOL/ex/Perm.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Permutations: example of an inductive definition
*)
Perm = List +
consts perm :: "('a list * 'a list) set"
syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50)
translations
"x <~~> y" == "(x,y) : perm"
inductive perm
intrs
Nil "[] <~~> []"
swap "y#x#l <~~> x#y#l"
Cons "xs <~~> ys ==> z#xs <~~> z#ys"
trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs"
end