changeset 25750  4e796867ccb5 
parent 17480  fd19f77dcf60 
child 33615  261abc2e3155 
25749:10e7feb4e595  25750:4e796867ccb5 

6 Modifed version of Lawrence Paulson's FOL that contains proof terms. 
6 Modifed version of Lawrence Paulson's FOL that contains proof terms. 
7 
7 
8 Presence of unknown proof term means that matching does not behave as expected. 
8 Presence of unknown proof term means that matching does not behave as expected. 
9 *) 
9 *) 
10 
10 
11 val banner = "FirstOrder Logic with Natural Deduction with Proof Terms"; 
11 use_thy "FOLP"; 
12 writeln banner; 

13 
12 
14 use_thy "FOLP"; 