<commit_before>(*  Title: 	HOL/ex/Perm.thy
    ID:         $Id$
    Author: 	<NAME>, 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)

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<commit_msg>Corrected mixfix declaration of @perm<commit_after>(*  Title: 	HOL/ex/Perm.thy
    ID:         $Id$
    Author: 	<NAME>, 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
{'fraction_non_alphanumeric': 0.2089795918367347, 'fraction_numerical': 0.014693877551020407, 'mean_word_length': 2.7492354740061162, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '191498', 'n_tokens_mistral': 520, 'n_tokens_neox': 491, 'n_words': 133}