### [ProofPower] any recommended ml editor

Hi, We plan to start a project based on proofpower. So we want to have a look at the source code, in particular those ml files. I wonder that if there is a recommended editor which can access/organise the source code for a developer. Currently I'm switching between JEditor and vi in xterm,

### [ProofPower] ml library functions from pp command line

Hi, I'm trying to build a programme on the top of proof power with the pp interface. I need a full polyML library from the pp interface, but I can't use some functions which are defined in polyML, e.g List.exists. Any suggestion ? Thanks in advance. best, Yuhui -- The University of

### [ProofPower] load proof power with PolyML

Hi, I wonder if is possible to load proof power from polyML directly, perhaps by PolyML.make with the proof power source code. The fact is that we want to build a system which proof power will be in the middle of the architecture, i.e some_libraries -- proofpower -- another_component_with_UI.

### Re: [ProofPower] load proof power with PolyML

2013, at 14:24, Yuhui Lin wrote: Hi, I wonder if is possible to load proof power from polyML directly, perhaps by PolyML.make with the proof power source code. I have never tried PolyML.make. There is no reason why you shouldn't compile the ProofPower source code by loading it in from

### [ProofPower] use library function with special symbol

Hi, I'm currently developing a system on the top of proof power. I get an error when reading a ml file with the keyword use in xpp. The error is caused by the use of a library function containing a special symbol, i.e. dest_simple_%lambda%. I am sure all the codes in the ML file is OK, as

### [ProofPower] use and use_file

Hi, I notice that some function names need to be changed when using the key word 'use_file' to include ML files, e.g. EQUAL becomes E%Q%UAL. I wonder why ? Is there anything else I need to keep in mind when using use_fie ? Many thanks. best, Yuhui -- The University of Edinburgh is a

### [ProofPower] AVoCS 2015: Second Call for Papers

, Imperial College London, UK Peter Ölveczky, University of Oslo, Norway ORGANISERS Gudmund Grov, Heriot-Watt University, UK Andrew Ireland, Heriot-Watt University, UK Yuhui Lin, Heriot-Watt University, UK (Local arrangements and publicity chair) STEERING COMMITTEE Michael Goldsmith

### [ProofPower] AVoCS 2015: Extended Paper Deadline

, UK Andrew Ireland, Heriot-Watt University, UK Yuhui Lin, Heriot-Watt University, UK (local arrangements and publicity chair) STEERING COMMITTEE Michael Goldsmith, University of Oxford, UK Stephan Merz, INRIA Nancy LORIA, France Markus Roggenbach, Swansea University, UK - We

### [ProofPower] apply conditional rewriting

Hi, How can I apply a conditional rewrite rule in proof power. For example, applying the following thm: forall x,y, z | x y dot x - y + z = x + z -y where x y is the condition, to generate the following two subgoals: 1) x y 2) goal [x - y + z / x + z -y] Also, I wonder is there any

### [ProofPower] error msg when instantiating quantifier in asm

Dear all, I get the following error when I tried to instantiated a forall quantifier in an assumption which I inserted using asm_tac. Exception Fail * Trying to instantiate type variable 'a, which occurs in assumption list [z_∀_elim.6006] * raised The following dummy example can replay this