<commit_before>(*  Title:      HOL/HOL.thy
    Author:     <NAME>, <NAME>, and <NAME>
*)

header {* The basis of Higher-Order Logic *}

theory HOL
imports Pure
uses
  ("Tools/hologic.ML")
  "~~/src/Tools/IsaPlanner/zipper.ML"
  "~~/src/Tools/IsaPlanner/isand.ML"
  "~~/src/Tools/IsaPlanner/rw_tools.ML"
  "~~/src/Tools/IsaPlanner/rw_inst.ML"
  "~~/src/Provers/project_rule.ML"
  "~~/src/Provers/hypsubst.ML"
  "~~/src/Provers/splitter.ML"
  "~~/src/Provers/classical.ML"
  "~~/src/Provers/blast.ML"
  "~~/src/Provers/clasimp.ML"
  "~~/src/Provers/coherent.ML"
  "~~/src/Provers/eqsubst.ML"
  "~~/src/Provers/quantifier1.ML"
  ("Tools/simpdata.ML")
  "~~/src/Tools/random_word.ML"
  "~~/src/Tools/atomize_elim.ML"
  "~~/src/Tools/induct.ML"
  ("~~/src/Tools/induct_tacs.ML")
  "~~/src/Tools/value.ML"
  "~~/src/Tools/code/code_name.ML"
  "~~/src/Tools/code/code_funcgr.ML"
  "~~/src/Tools/code/code_thingol.ML"
  "~~/src/Tools/code/code_printer.ML"
  "~~/src/Tools/code/code_target.ML"
  "~~/src/Tools/code/code_ml.ML"
  "~~/src/Tools/code/code_haskell.ML"
  "~~/src/Tools/nbe.ML"
  ("Tools/recfun_codegen.ML")
begin

subsection {* Primitive logic *}

subsubsection {* Core syntax *}

classes type
defaultsort type
setup {* ObjectLogic.add_base_sort @{sort type} *}

arities
  "fun" :: (type, type) type
  itself :: (type) type<commit_msg>experimental inclusion of new wellsorting algorithm for code equations<commit_after>(*  Title:      HOL/HOL.thy
    Author:     <NAME>, <NAME>, and <NAME>
*)

header {* The basis of Higher-Order Logic *}

theory HOL
imports Pure
uses
  ("Tools/hologic.ML")
  "~~/src/Tools/IsaPlanner/zipper.ML"
  "~~/src/Tools/IsaPlanner/isand.ML"
  "~~/src/Tools/IsaPlanner/rw_tools.ML"
  "~~/src/Tools/IsaPlanner/rw_inst.ML"
  "~~/src/Provers/project_rule.ML"
  "~~/src/Provers/hypsubst.ML"
  "~~/src/Provers/splitter.ML"
  "~~/src/Provers/classical.ML"
  "~~/src/Provers/blast.ML"
  "~~/src/Provers/clasimp.ML"
  "~~/src/Provers/coherent.ML"
  "~~/src/Provers/eqsubst.ML"
  "~~/src/Provers/quantifier1.ML"
  ("Tools/simpdata.ML")
  "~~/src/Tools/random_word.ML"
  "~~/src/Tools/atomize_elim.ML"
  "~~/src/Tools/induct.ML"
  ("~~/src/Tools/induct_tacs.ML")
  "~~/src/Tools/value.ML"
  "~~/src/Tools/code/code_name.ML"
  "~~/src/Tools/code/code_wellsorted.ML"
  "~~/src/Tools/code/code_thingol.ML"
  "~~/src/Tools/code/code_printer.ML"
  "~~/src/Tools/code/code_target.ML"
  "~~/src/Tools/code/code_ml.ML"
  "~~/src/Tools/code/code_haskell.ML"
  "~~/src/Tools/nbe.ML"
  ("Tools/recfun_codegen.ML")
begin

subsection {* Primitive logic *}

subsubsection {* Core syntax *}

classes type
defaultsort type
setup {* ObjectLogic.add_base_sort @{sort type} *}

arities
  "fun" :: (type, type) type
  itself :: (type) type
{'fraction_non_alphanumeric': 0.21191085129704054, 'fraction_numerical': 0.0007307270734380709, 'mean_word_length': 3.68034188034188, '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': '570302', 'n_tokens_mistral': 1223, 'n_tokens_neox': 1208, 'n_words': 149}