<commit_before>
(* Author: <NAME>, <NAME> *)

header {* A huge collection of equations to generate code from *}

theory Candidates
imports
  Complex_Main
  Library
  List_Prefix
  "~~/src/HOL/Number_Theory/Primes"
  "~~/src/HOL/ex/Records"
begin

inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    empty: "sublist [] xs"
  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"<commit_msg>modernized imports;<commit_after>
(* Author: <NAME>, T<NAME> *)

header {* A huge collection of equations to generate code from *}

theory Candidates
imports
  Complex_Main
  Library
  "~~/src/HOL/Library/List_Prefix"
  "~~/src/HOL/Number_Theory/Primes"
  "~~/src/HOL/ex/Records"
begin

inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    empty: "sublist [] xs"
  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
{'fraction_non_alphanumeric': 0.15166340508806261, 'fraction_numerical': 0.0, 'mean_word_length': 4.064356435643564, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 15, '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': '1999271', 'n_tokens_mistral': 393, 'n_tokens_neox': 370, 'n_words': 110}