blob: 51a09b9cda213c670cf8bdfcacb48f7d4822b021 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* This library implements an automated method, DefineDiv, which generates
definitions by means of the fixed-point operator ‘fix’ introduced in
‘divDefScript’.
For examples of how to use the fixed-point operator step by step on
hand-written examples, see divDefExampleTheory.
The current file is organized so as to follow the steps detailed in
divDefExampleTheory.
For examples of how to use DefiveDiv, see divDefLibExampleScript.
*)
signature divDefLib =
sig
include Abbrev
val DefineDiv : term quotation -> thm list
end
|
