<commit_before>(*  Title:      HOL/MetisTest/TransClosure.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory

Testing the metis method
*)

theory TransClosure
imports Main
begin

types addr = nat

datatype val
  = Unit        -- "dummy result value of void expressions"
  | Null        -- "null reference"
  | Bool bool   -- "Boolean value"
  | Intg int    -- "integer value" 
  | Addr addr   -- "addresses of objects in the heap"

consts R::"(addr \<times> addr) set"

consts f:: "addr \<Rightarrow> val"
<commit_msg>dropped Id<commit_after>(*  Title:      HOL/MetisTest/TransClosure.thy
    Author:     <NAME>, Cambridge University Computer Laboratory

Testing the metis method
*)

theory TransClosure
imports Main
begin

types addr = nat

datatype val
  = Unit        -- "dummy result value of void expressions"
  | Null        -- "null reference"
  | Bool bool   -- "Boolean value"
  | Intg int    -- "integer value" 
  | Addr addr   -- "addresses of objects in the heap"

consts R::"(addr \<times> addr) set"

consts f:: "addr \<Rightarrow> val"

{'fraction_non_alphanumeric': 0.10733944954128441, 'fraction_numerical': 0.0, 'mean_word_length': 2.7363013698630136, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, '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': '4215060', 'n_tokens_mistral': 355, 'n_tokens_neox': 334, 'n_words': 121}