src/LCF/ex.ML
changeset 203 4a213aaca3d9
parent 0 a5a9c433f639
child 420 1e0f1973536d
equal deleted inserted replaced
202:4e68398cdc06 203:4a213aaca3d9
    12 proof_timing := true;
    12 proof_timing := true;
    13 
    13 
    14 (***  Section 10.4  ***)
    14 (***  Section 10.4  ***)
    15 
    15 
    16 val ex_thy = extend_theory thy "Ex 10.4"
    16 val ex_thy = extend_theory thy "Ex 10.4"
    17 ([], [], [], [],
    17 ([], [], [], [], [],
    18  [(["P"], "'a => tr"),
    18  [(["P"], "'a => tr"),
    19   (["G","H"], "'a => 'a"),
    19   (["G","H"], "'a => 'a"),
    20   (["K"], "('a => 'a) => ('a => 'a)")
    20   (["K"], "('a => 'a) => ('a => 'a)")
    21  ],
    21  ],
    22  None)
    22  None)
    54 
    54 
    55 
    55 
    56 (***  Example 3.8  ***)
    56 (***  Example 3.8  ***)
    57 
    57 
    58 val ex_thy = extend_theory thy "Ex 3.8"
    58 val ex_thy = extend_theory thy "Ex 3.8"
    59 ([], [], [], [],
    59 ([], [], [], [], [],
    60  [(["P"], "'a => tr"),
    60  [(["P"], "'a => tr"),
    61   (["F","G"], "'a => 'a"),
    61   (["F","G"], "'a => 'a"),
    62   (["H"], "'a => 'b => 'b"),
    62   (["H"], "'a => 'b => 'b"),
    63   (["K"], "('a => 'b => 'b) => ('a => 'b => 'b)")
    63   (["K"], "('a => 'b => 'b) => ('a => 'b => 'b)")
    64  ],
    64  ],
    84 
    84 
    85 
    85 
    86 (*** Addition with fixpoint of successor ***)
    86 (*** Addition with fixpoint of successor ***)
    87 
    87 
    88 val ex_thy = extend_theory thy "fix ex"
    88 val ex_thy = extend_theory thy "fix ex"
    89 ([], [], [], [],
    89 ([], [], [], [], [],
    90  [(["s"], "'a => 'a"),
    90  [(["s"], "'a => 'a"),
    91   (["p"], "'a => 'a => 'a")
    91   (["p"], "'a => 'a => 'a")
    92  ],
    92  ],
    93  None)
    93  None)
    94 [ ("p_strict", "p(UU) = UU"),
    94 [ ("p_strict", "p(UU) = UU"),