equal
deleted
inserted
replaced
1 (* Title: FOL/ex/Intuitionistic |
1 (* Title: FOL/ex/Intuitionistic.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
5 *) |
4 *) |
6 |
5 |
7 header{*Intuitionistic First-Order Logic*} |
6 header {* Intuitionistic First-Order Logic *} |
8 |
7 |
9 theory Intuitionistic imports IFOL begin |
8 theory Intuitionistic |
|
9 imports IFOL |
|
10 begin |
10 |
11 |
11 (* |
12 (* |
12 Single-step ML commands: |
13 Single-step ML commands: |
13 by (IntPr.step_tac 1) |
14 by (IntPr.step_tac 1) |
14 by (biresolve_tac safe_brls 1); |
15 by (biresolve_tac safe_brls 1); |
420 lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
421 lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
421 by (tactic{*IntPr.fast_tac 1*}) |
422 by (tactic{*IntPr.fast_tac 1*}) |
422 |
423 |
423 end |
424 end |
424 |
425 |
425 |
|