File: example.l

package info (click to toggle)
proofgeneral 3.7-4
  • links: PTS
  • area: main
  • in suites: squeeze
  • size: 9,328 kB
  • ctags: 4,317
  • sloc: lisp: 49,786; makefile: 466; sh: 339; perl: 205; ansic: 43
file content (15 lines) | stat: -rw-r--r-- 231 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
(*
    Example proof script for Lego Proof General.
 
    example.l,v 9.0 2008/01/30 15:22:19 da Exp
*)

Module example Import lib_logic;

Goal {A,B:Prop}(A /\ B) -> (B /\ A);
intros;
Refine H;
intros;
andI;
Immed;
Save and_comms;