[Hol-info] Multiple PhD positions in Information Security at ETH Zurich

The Institute of Information Security headed by Prof. David Basin at ETH Zurich has multiple open positions for PhD students on research projects in the area of formal methods for information security. We are looking for enthusiastic outstanding Computer Science or Mathematics students with a stro

Re: [Hol-info] [SPAM] some questions about the use of THEN and THENL in HOL4

The tactic (tac1 THEN tac2) applies tac2 to all subgoals generated by tac1. On 22 December 2015 at 23:05, Ada wrote: > Hey guys, > > I am learning to use HOL4. In listTheory , I found that: > val DROP_0 = store_thm( > "DROP_0", > ``DROP 0 l = l``, > Induct_on `l` THEN SRW_TAC [] []); > I w

[Hol-info] [SPAM] some questions about the use of THEN and THENL in HOL4

Hey guys, I am learning to use HOL4. In listTheory , I found that: val DROP_0 = store_thm( "DROP_0", ``DROP 0 l = l``, Induct_on `l` THEN SRW_TAC [] []); I was wondering that after "Induct_on `l`", there should be two subgoals. But the following was "THEN SRW_TAC [] []", I thought it sho