<commit_before>(*  Title: 	FOLP/ROOT
    ID:         $Id$
    Author: 	<NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Modifed version of Lawrence Paulson's FOL that contains proof terms.

Presence of unknown proof term means that matching does not behave as expected.
*)

val banner = "First-Order Logic with Natural Deduction with Proof Terms";

writeln banner;

init_thy_reader();

print_depth 1;  
use_thy "IFOLP";
use_thy "FOLP";

use "../Provers/hypsubst.ML";
use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
use "simp.ML";	         (* Patched 'cos matching won't instantiate proof *)
use "../Provers/ind.ML";
<commit_msg>Loads the local hypsubst.ML.  No longer loads ../Provers/ind.ML, which was never used.<commit_after>(*  Title: 	FOLP/ROOT
    ID:         $Id$
    Author: 	<NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Modifed version of Lawrence Paulson's FOL that contains proof terms.

Presence of unknown proof term means that matching does not behave as expected.
*)

val banner = "First-Order Logic with Natural Deduction with Proof Terms";

writeln banner;

init_thy_reader();

print_depth 1;  
use_thy "IFOLP";
use_thy "FOLP";

use "hypsubst.ML";
use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
use "simp.ML";	         (* Patched 'cos matching won't instantiate proof *)

{'fraction_non_alphanumeric': 0.09619377162629758, 'fraction_numerical': 0.006920415224913495, 'mean_word_length': 3.6948051948051948, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, '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': '3344775', 'n_tokens_mistral': 469, 'n_tokens_neox': 437, 'n_words': 165}