equal
deleted
inserted
replaced
9 /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml |
9 /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml |
10 *) |
10 *) |
11 |
11 |
12 structure ParContract = Inductive_Fun |
12 structure ParContract = Inductive_Fun |
13 (val thy = Contract.thy; |
13 (val thy = Contract.thy; |
|
14 val thy_name = "ParContract"; |
14 val rec_doms = [("parcontract","comb*comb")]; |
15 val rec_doms = [("parcontract","comb*comb")]; |
15 val sintrs = |
16 val sintrs = |
16 ["[| p:comb |] ==> p =1=> p", |
17 ["[| p:comb |] ==> p =1=> p", |
17 "[| p:comb; q:comb |] ==> K#p#q =1=> p", |
18 "[| p:comb; q:comb |] ==> K#p#q =1=> p", |
18 "[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)", |
19 "[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)", |