isabelle: src/HOL/Lex/Scanner.ML@e84a0b941beb (annotated)

4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	1	(* Title: HOL/Lex/Scanner.ML
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	2	ID: $Id$
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	3	Author: Tobias Nipkow
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	4	Copyright 1998 TUM
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	5	*)
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	6
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	7	Goal
5323 028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	8	"DA.accepts (na2da(rexp2na r)) w = (w : lang r)";
028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	9	by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1);
028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	10	qed "accepts_na2da_rexp2na";
028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	11
028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	12	Goal
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	13	"DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	14	by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: diff changeset	15	qed "accepts_nae2da_rexp2nae";

author	paulson
	Mon, 24 May 1999 15:44:20 +0200
changeset 6701	e84a0b941beb
parent 5323	028e00595280
permissions	-rw-r--r--